Theorem sylanb 449

Description: A syllogism inference.

Hypotheses

Ref	Expression
sylan.1	|- ((ph /\ ps) -> ch)
sylanb.2	|- (th <-> ph)

Assertion

Ref	Expression
sylanb	|- ((th /\ ps) -> ch)

Proof of Theorem sylanb

Step	Hyp	Ref	Expression
1		sylan.1	. 2 |- ((ph /\ ps) -> ch)
2		sylanb.2	. . 3 |- (th <-> ph)
3	2	biimp 151	. 2 |- (th -> ph)
4	1, 3	sylan 448	1 |- ((th /\ ps) -> ch)

Syntax hints:   -> wi 3   <-> wb 146   /\ wa 223

This theorem is referenced by:  syl2anb 455  2euex 1441  2exeu 1446  eqtr2t 1493  sspsstr 2151  disjne 2315  ordon 2987  ordsucss 3069  ordsucelsuc 3073  funex 3608  fssres 3643  fvimacnvi 3804  tz7.48lem 3955  1st2nd 4108  oeworde 4220  nnmsucr 4240  erref 4275  mapxpen 4495  php 4513  php3OLD 4516  php4 4517  omsucdom 4523  isfinite2OLD 4546  fodomfiOLD 4566  brdom3 4801  cfeq0 4914  pre-axsup 5291  divmul13t 5782  lemuldivtOLD 5875  uzindOLD 6208  qbtwnxr 6279  faclbnd 6945  faclbnd3 6947  fsum0clt 7016  ser0clt 7046  ser1clt 7047  binomlem5 7070  climaddlem3 7116  climmullem8 7127  climcmplem 7137  isumnn0nna 7208  mulc1cncf 7279  ruclem13 7522  opnin 7869  fsumcnlem 7989  grpidinvlem3 8050  mulid 8132  ipasslem3 8492  hilid 9028  occllem6 9178  spanun 9467  5oalem3 9601  5oalem5 9603  mdslmd1lem2 10253

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 147  df-an 225

Copyright terms: Public domain