Theorem sylanb 472

Description: A syllogism inference. (Contributed by NM, 18-May-1994.)

Hypotheses

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

Assertion

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

Proof of Theorem sylanb

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

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 369

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

This theorem depends on definitions:  df-bi 185  df-an 371

This theorem is referenced by:  syl2anb  479  anabsan  809  eqtr2  2461  pm13.181  2699  rmob  3301  sspsstr  3476  disjne  3739  seex  4698  tron  4757  xpcan2  5290  fssres  5593  funbrfvb  5749  funopfvb  5750  fvco  5782  fvimacnvi  5832  ffvresb  5889  funressn  5910  funresdfunsn  5935  fvtp2  5941  fvtp2g  5944  fnex  5959  funex  5960  ordsucss  6444  ordsucelsuc  6448  1st2nd  6635  frxp  6697  dftpos4  6779  tz7.48lem  6911  nnmsucr  7079  nnmcan  7088  xpmapenlem  7493  php  7510  php4  7513  omsucdomOLD  7521  isfinite2  7585  wofib  7774  r1limg  7993  r1pwcl  8069  cardmin2  8183  zornn0g  8689  intgru  8996  supsrlem  9293  uzindOLD  10751  fnn0ind  10756  uztrn2  10893  nnwo  10935  irradd  10992  qbtwnxr  11185  xltnegi  11201  xaddnemnf  11219  xaddnepnf  11220  xaddcom  11223  xnegdi  11226  elioore  11345  uzsubsubfz1  11487  fzo1fzo0n0  11603  elfzonelfzo  11642  leexp2  11933  faclbnd  12081  faclbnd3  12083  brfi1uzind  12234  swrdccat3b  12402  dvdslelem  13592  divalglem1  13613  isprm2lem  13785  dvdsprime  13791  pcgcd  13959  cntri  15863  efgsrel  16246  xrsdsreclb  17875  znf1o  17999  restuni  18781  stoig  18782  restperf  18803  resstps  18806  pnfnei  18839  mnfnei  18840  cnnei  18901  cmpsublem  19017  tx1stc  19238  xkopt  19243  isfcls  19597  tgioo  20388  opnreen  20423  iscmet3  20819  dyaddisj  21091  limcmpt  21373  degltlem1  21558  ulmdvlem3  21882  lgsdi  22686  eupath2lem3  23615  grpoidinvlem3  23708  ipasslem3  24248  spanuni  24962  5oalem3  25074  5oalem5  25076  mdslmd1lem2  25745  mptct  26033  mptctf  26036  xaddeq0  26061  ordtconlem1  26369  esumcvg  26550  measres  26651  measdivcstOLD  26653  measdivcst  26654  probun  26817  dfon2lem9  27619  noreson  27816  funpartfun  27989  cgrxfr  28101  segcon2  28151  brsegle2  28155  seglecgr12im  28156  segletr  28160  ftc1anclem5  28490  ftc1anc  28494  nn0prpw  28537  comppfsc  28598  exlimddvfi  28949  prtlem11  29030  mzpclall  29082  funbrafvb  30081  funopafvb  30082  afvco2  30101  2wlkonotv  30415  clwlkfclwwlk  30536  dmatsubcl  30896  bj-seex  32445