Theorem sylanb 498

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	biimpi 168	. 2 |- (th -> ph)
4	1, 3	sylan 497	1 |- ((th /\ ps) -> ch)

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240

This theorem is referenced by:  syl2anb 504  2euexOLD 1845  2exeu 1850  eqtr2 1905  eqtr2OLD 1906  pm13.181 2086  sspsstr 2715  disjne 2919  disjneOLD 2920  tron 3681  ordsucss 3899  ordsucelsuc 3902  ordsucelsucOLD 3903  xpcan2 4350  fnex 4535  funex 4537  fssres 4582  fvimacnvi 4777  1st2nd 5048  tz7.48lem 5164  oeworde 5268  nnmsucr 5295  nnmsucrOLD 5296  erref 5333  mapxpen 5589  php 5607  php4 5610  omsucdom 5616  isfinite2 5639  fodomfi 5656  brdom3 5963  cfeq0 6062  pre-axsup 6444  addgegt0i 6779  uzindOLD 7420  qbtwnxr 7460  faclbnd 8197  faclbnd3 8199  fsum0cl 8276  ser0cl 8306  ser1cl 8307  binomlem5 8330  climaddlem3 8376  climmullem8 8387  climcmplem 8397  isumnn0nnai 8469  mulc1cncf 8541  ruclem13 8791  opnin 9146  fsumcnlem 9267  grpidinvlem3 9330  mulid 9440  vacnlem3 9669  ipasslem3 9833  subtopmetlem 10255  extbas1 10291  usinuniop 10341  hilid 10661  occllem6 10811  spanuni 11100  5oalem3 11236  5oalem5 11238  mdslmd1lem2 11898  bnj1139 12937  fnn0ind 13611  seq1resval2 13618  dvdslelem 13692  divalglem1 13697  eucalgcvga 13754  isprm2lem 13774  dfon2lem9 13857  frxp 13951  axbday 14012  cntrsetlem 14999  compsublem 15430  compfipin0lem 15435  comppfsc 15517  ufprim 15569  difxp 15690  zornn0 15764  frminex 15773  sdclem1 15809  sdclem2 15810  heiborlem23 15977  heiborlem29 15983  rrnmet 16016  rrndstprj1 16017  rrndstprj2 16018  rrntotbndlem1 16020  rrntotbndlem2 16021  rrntotbnd 16022  pcopt 16084  pcoass 16085  prtlem11 16268  pm13.181OLD 16372  grpidinvlem3NEW 17111

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 164  df-an 242

Copyright terms: Public domain