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  813  eqtr2  2470  pm13.181  2755  rmob  3416  sspsstr  3594  disjne  3858  seex  4832  tron  4891  xpcan2  5434  fssres  5741  funbrfvb  5900  funopfvb  5901  fvco  5934  fvimacnvi  5986  ffvresb  6047  funressn  6069  funresdfunsn  6098  fvtp2  6104  fvtp2g  6107  fnex  6124  funex  6125  ordsucss  6638  ordsucelsuc  6642  1st2nd  6831  frxp  6895  dftpos4  6976  tz7.48lem  7108  nnmsucr  7276  nnmcan  7285  xpmapenlem  7686  php  7703  php4  7706  omsucdomOLD  7715  isfinite2  7780  wofib  7973  r1limg  8192  r1pwcl  8268  cardmin2  8382  zornn0g  8888  intgru  9195  supsrlem  9491  uzindOLD  10964  fnn0ind  10970  uztrn2  11109  nnwo  11158  irradd  11217  qbtwnxr  11410  xltnegi  11426  xaddnemnf  11444  xaddnepnf  11445  xaddcom  11448  xnegdi  11451  elioore  11570  uzsubsubfz1  11719  fzo1fzo0n0  11846  elfzonelfzo  11894  leexp2  12202  faclbnd  12350  faclbnd3  12352  brfi1uzind  12514  swrdccat3b  12703  dvdslelem  14012  divalglem1  14034  isprm2lem  14206  dvdsprime  14212  pcgcd  14383  cntri  16347  efgsrel  16731  xrsdsreclb  18444  znf1o  18568  restuni  19641  stoig  19642  restperf  19663  resstps  19666  pnfnei  19699  mnfnei  19700  cnnei  19761  cmpsublem  19877  comppfsc  20011  tx1stc  20129  xkopt  20134  isfcls  20488  tgioo  21279  opnreen  21314  iscmet3  21710  dyaddisj  21983  limcmpt  22265  degltlem1  22450  ulmdvlem3  22775  lgsdi  23585  clwlkfclwwlk  24822  2wlkonotv  24855  eupath2lem3  24957  grpoidinvlem3  25186  ipasslem3  25726  spanuni  26440  5oalem3  26552  5oalem5  26554  mdslmd1lem2  27223  mptct  27519  mptctf  27522  xaddeq0  27551  ordtconlem1  27884  esumcvg  28070  measres  28171  measdivcstOLD  28173  measdivcst  28174  probun  28336  elmpps  28911  dfon2lem9  29199  noreson  29396  funpartfun  29569  cgrxfr  29681  segcon2  29731  brsegle2  29735  seglecgr12im  29736  segletr  29740  ftc1anclem5  30070  ftc1anc  30074  nn0prpw  30117  exlimddvfi  30503  prtlem11  30583  mzpclall  30635  funbrafvb  32195  funopafvb  32196  afvco2  32215  fundmfibi  32265  usgfis  32400  usgfisALT  32404  4an31  33135  bj-seex  34374