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  811  eqtr2  2494  pm13.181  2779  rmob  3431  sspsstr  3609  disjne  3872  seex  4842  tron  4901  xpcan2  5442  fssres  5749  funbrfvb  5908  funopfvb  5909  fvco  5941  fvimacnvi  5993  ffvresb  6050  funressn  6072  funresdfunsn  6101  fvtp2  6107  fvtp2g  6110  fnex  6125  funex  6126  ordsucss  6631  ordsucelsuc  6635  1st2nd  6827  frxp  6890  dftpos4  6971  tz7.48lem  7103  nnmsucr  7271  nnmcan  7280  xpmapenlem  7681  php  7698  php4  7701  omsucdomOLD  7710  isfinite2  7774  wofib  7966  r1limg  8185  r1pwcl  8261  cardmin2  8375  zornn0g  8881  intgru  9188  supsrlem  9484  uzindOLD  10951  fnn0ind  10956  uztrn2  11095  nnwo  11143  irradd  11202  qbtwnxr  11395  xltnegi  11411  xaddnemnf  11429  xaddnepnf  11430  xaddcom  11433  xnegdi  11436  elioore  11555  uzsubsubfz1  11704  fzo1fzo0n0  11828  elfzonelfzo  11876  leexp2  12184  faclbnd  12332  faclbnd3  12334  brfi1uzind  12494  swrdccat3b  12680  dvdslelem  13885  divalglem1  13907  isprm2lem  14079  dvdsprime  14085  pcgcd  14256  cntri  16163  efgsrel  16548  xrsdsreclb  18233  znf1o  18357  restuni  19429  stoig  19430  restperf  19451  resstps  19454  pnfnei  19487  mnfnei  19488  cnnei  19549  cmpsublem  19665  tx1stc  19886  xkopt  19891  isfcls  20245  tgioo  21036  opnreen  21071  iscmet3  21467  dyaddisj  21740  limcmpt  22022  degltlem1  22207  ulmdvlem3  22531  lgsdi  23335  clwlkfclwwlk  24520  2wlkonotv  24553  eupath2lem3  24655  grpoidinvlem3  24884  ipasslem3  25424  spanuni  26138  5oalem3  26250  5oalem5  26252  mdslmd1lem2  26921  mptct  27213  mptctf  27216  xaddeq0  27241  ordtconlem1  27542  esumcvg  27732  measres  27833  measdivcstOLD  27835  measdivcst  27836  probun  27998  dfon2lem9  28800  noreson  28997  funpartfun  29170  cgrxfr  29282  segcon2  29332  brsegle2  29336  seglecgr12im  29337  segletr  29341  ftc1anclem5  29671  ftc1anc  29675  nn0prpw  29718  comppfsc  29779  exlimddvfi  30130  prtlem11  30211  mzpclall  30263  funbrafvb  31708  funopafvb  31709  afvco2  31728  fundmfibi  31780  usgfis  31915  usgfisALT  31919  bj-seex  33572