Theorem sylanb 474

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

Syntax hints:   -> wi 4   <-> wb 187   /\ wa 370

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 188  df-an 372

This theorem is referenced by:  syl2anb  481  anabsan  820  eqtr2  2449  pm13.181  2732  rmob  3391  sspsstr  3570  disjne  3840  seex  4816  xpcan2  5293  tron  5465  fssres  5766  funbrfvb  5923  funopfvb  5924  fvco  5957  fvimacnvi  6011  ffvresb  6069  funressn  6092  funresdfunsn  6121  fvtp2  6127  fvtp2g  6130  fnex  6147  funex  6148  ordsucss  6659  ordsucelsuc  6663  1st2nd  6853  frxp  6917  dftpos4  7003  tz7.48lem  7169  nnmsucr  7337  nnmcan  7346  xpmapenlem  7748  php  7765  php4  7768  isfinite2  7838  fundmfibi  7864  fiinfcl  8026  wofib  8069  r1limg  8250  r1pwcl  8326  cardmin2  8440  zornn0g  8942  intgru  9246  supsrlem  9542  fnn0ind  11041  uztrn2  11183  nnwo  11231  irradd  11295  qbtwnxr  11500  xltnegi  11516  xaddnemnf  11534  xaddnepnf  11535  xaddcom  11538  xnegdi  11541  elioore  11673  uzsubsubfz1  11829  fzo1fzo0n0  11964  elfzonelfzo  12017  leexp2  12333  faclbnd  12481  faclbnd3  12483  fi1uzind  12654  brfi1uzind  12655  opfi1uzind  12658  swrdccat3b  12854  dvdslelem  14348  divalglem1  14371  isprm2lem  14630  dvdsprime  14636  pcgcd  14826  cntri  16983  efgsrel  17383  xrsdsreclb  19014  znf1o  19120  restuni  20176  stoig  20177  restperf  20198  resstps  20201  pnfnei  20234  mnfnei  20235  cnnei  20296  cmpsublem  20412  comppfsc  20545  tx1stc  20663  xkopt  20668  isfcls  21022  tgioo  21812  opnreen  21847  iscmet3  22261  dyaddisj  22552  limcmpt  22836  degltlem1  23019  ulmdvlem3  23355  lgsdi  24258  clwlkfclwwlk  25570  2wlkonotv  25603  eupath2lem3  25705  grpoidinvlem3  25932  ipasslem3  26472  spanuni  27195  5oalem3  27307  5oalem5  27309  mdslmd1lem2  27977  mptct  28308  mptctf  28311  xaddeq0  28336  ordtconlem1  28738  esumcvg  28915  ldgenpisyslem1  28993  measres  29052  measdivcstOLD  29054  measdivcst  29055  probun  29260  elmpps  30219  dfon2lem9  30444  noreson  30554  funpartfun  30715  cgrxfr  30827  segcon2  30877  brsegle2  30881  seglecgr12im  30882  segletr  30886  nn0prpw  30984  bj-seex  31495  ptrecube  31904  poimirlem28  31932  ftc1anclem5  31985  ftc1anc  31989  exlimddvfi  32326  prtlem11  32406  mzpclall  35538  4an31  36824  iundjiun  38206  funbrafvb  38528  funopafvb  38529  afvco2  38548  cusgrres  39266  usgfis  39378  usgfisALT  39382