Theorem sylanb 479

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 199	. 2 |- ( ph -> ps )
3		sylanb.2	. 2 |- ( ( ps /\ ch ) -> th )
4	2, 3	sylan 478	1 |- ( ( ph /\ ch ) -> th )

Syntax hints:   -> wi 4   <-> wb 189   /\ wa 375

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 190  df-an 377

This theorem is referenced by:  syl2anb  486  anabsan  827  eqtr2  2482  pm13.181  2718  rmob  3371  sspsstr  3550  disjne  3822  seex  4819  xpcan2  5296  tron  5469  fssres  5776  funbrfvb  5934  funopfvb  5935  fvco  5969  fvimacnvi  6024  ffvresb  6083  funressn  6106  funresdfunsn  6135  fvtp2  6141  fvtp2g  6144  fnex  6162  funex  6163  ordsucss  6677  ordsucelsuc  6681  1st2nd  6871  frxp  6938  dftpos4  7023  tz7.48lem  7189  nnmsucr  7357  nnmcan  7366  xpmapenlem  7770  php  7787  php4  7790  isfinite2  7860  fundmfibi  7886  fiinfcl  8048  wofib  8091  r1limg  8273  r1pwcl  8349  cardmin2  8463  zornn0g  8966  intgru  9270  supsrlem  9566  fnn0ind  11068  uztrn2  11210  nnwo  11258  irradd  11322  qbtwnxr  11527  xltnegi  11543  xaddnemnf  11561  xaddnepnf  11562  xaddcom  11565  xnegdi  11568  elioore  11700  uzsubsubfz1  11857  fzo1fzo0n0  11994  elfzonelfzo  12048  leexp2  12365  faclbnd  12513  faclbnd3  12515  fi1uzind  12689  brfi1uzind  12690  opfi1uzind  12693  swrdccat3b  12895  dvdslelem  14404  divalglem1  14427  isprm2lem  14686  dvdsprime  14692  pcgcd  14882  cntri  17039  efgsrel  17439  xrsdsreclb  19070  znf1o  19177  restuni  20233  stoig  20234  restperf  20255  resstps  20258  pnfnei  20291  mnfnei  20292  cnnei  20353  cmpsublem  20469  comppfsc  20602  tx1stc  20720  xkopt  20725  isfcls  21079  tgioo  21869  opnreen  21904  iscmet3  22318  dyaddisj  22610  limcmpt  22894  degltlem1  23077  ulmdvlem3  23413  lgsdi  24316  clwlkfclwwlk  25628  2wlkonotv  25661  eupath2lem3  25763  grpoidinvlem3  25990  ipasslem3  26530  spanuni  27253  5oalem3  27365  5oalem5  27367  mdslmd1lem2  28035  mptct  28354  mptctf  28357  xaddeq0  28382  ordtconlem1  28781  esumcvg  28958  ldgenpisyslem1  29036  measres  29095  measdivcstOLD  29097  measdivcst  29098  probun  29302  elmpps  30261  dfon2lem9  30487  noreson  30597  funpartfun  30760  cgrxfr  30872  segcon2  30922  brsegle2  30926  seglecgr12im  30927  segletr  30931  nn0prpw  31029  bj-seex  31572  ptrecube  31986  poimirlem28  32014  ftc1anclem5  32067  ftc1anc  32071  exlimddvfi  32408  prtlem11  32484  mzpclall  35615  4an31  36899  iundjiun  38403  funbrafvb  38793  funopafvb  38794  afvco2  38813  cusgrres  39655  usgfis  40127  usgfisALT  40131