Theorem sylanb 451

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 450	1 |- ((th /\ ps) -> ch)

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

This theorem is referenced by:  syl2anb 457  2euex 1444  2exeu 1449  eqtr2t 1496  sspsstr 2154  disjne 2319  ordon 2993  ordsucss 3075  ordsucelsuc 3079  funex 3614  fssres 3649  fvimacnvi 3810  tz7.48lem 3961  1st2nd 4114  oeworde 4226  nnmsucr 4246  erref 4281  mapxpen 4501  php 4519  php3OLD 4522  php4 4523  omsucdom 4528  isfinite2 4557  isfinite2OLD 4558  fodomfi 4575  fodomfiOLD 4576  brdom3 4811  cfeq0 4926  pre-axsup 5303  divmul13t 5784  lemuldivtOLD 5877  uzindOLD 6210  qbtwnxr 6280  faclbnd 6945  faclbnd3 6947  fsum0clt 7016  ser0clt 7046  ser1clt 7047  binomlem5 7070  climaddlem3 7116  climmullem8 7127  climcmplem 7137  isumnn0nna 7208  mulc1cncf 7279  ruclem13 7523  opnin 7866  fsumcnlem 7986  grpidinvlem3 8047  mulid 8128  ipasslem3 8488  hilid 9023  occllem6 9173  spanun 9462  5oalem3 9596  5oalem5 9598  mdslmd1lem2 10248

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