Theorem sylanb 470

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 469	1 |- ( ( ph /\ ch ) -> th )

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

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 369

This theorem is referenced by:  syl2anb  477  anabsan  811  eqtr2  2409  pm13.181  2694  rmob  3344  sspsstr  3523  disjne  3788  seex  4756  tron  4815  xpcan2  5354  fssres  5659  funbrfvb  5816  funopfvb  5817  fvco  5850  fvimacnvi  5903  ffvresb  5964  funressn  5986  funresdfunsn  6015  fvtp2  6021  fvtp2g  6024  fnex  6040  funex  6041  ordsucss  6552  ordsucelsuc  6556  1st2nd  6745  frxp  6809  dftpos4  6892  tz7.48lem  7024  nnmsucr  7192  nnmcan  7201  xpmapenlem  7603  php  7620  php4  7623  isfinite2  7693  wofib  7885  r1limg  8102  r1pwcl  8178  cardmin2  8292  zornn0g  8798  intgru  9103  supsrlem  9399  fnn0ind  10878  uztrn2  11018  nnwo  11066  irradd  11125  qbtwnxr  11320  xltnegi  11336  xaddnemnf  11354  xaddnepnf  11355  xaddcom  11358  xnegdi  11361  elioore  11480  uzsubsubfz1  11629  fzo1fzo0n0  11759  elfzonelfzo  11811  leexp2  12123  faclbnd  12270  faclbnd3  12272  brfi1uzind  12436  swrdccat3b  12632  dvdslelem  14032  divalglem1  14054  isprm2lem  14226  dvdsprime  14232  pcgcd  14403  cntri  16485  efgsrel  16869  xrsdsreclb  18578  znf1o  18681  restuni  19749  stoig  19750  restperf  19771  resstps  19774  pnfnei  19807  mnfnei  19808  cnnei  19869  cmpsublem  19985  comppfsc  20118  tx1stc  20236  xkopt  20241  isfcls  20595  tgioo  21386  opnreen  21421  iscmet3  21817  dyaddisj  22090  limcmpt  22372  degltlem1  22557  ulmdvlem3  22882  lgsdi  23724  clwlkfclwwlk  24965  2wlkonotv  24998  eupath2lem3  25100  grpoidinvlem3  25325  ipasslem3  25865  spanuni  26579  5oalem3  26691  5oalem5  26693  mdslmd1lem2  27361  mptct  27690  mptctf  27693  xaddeq0  27723  ordtconlem1  28060  esumcvg  28234  measres  28349  measdivcstOLD  28351  measdivcst  28352  probun  28541  elmpps  29122  dfon2lem9  29388  noreson  29585  funpartfun  29746  cgrxfr  29858  segcon2  29908  brsegle2  29912  seglecgr12im  29913  segletr  29917  ftc1anclem5  30260  ftc1anc  30264  nn0prpw  30307  exlimddvfi  30693  prtlem11  30773  mzpclall  30825  funbrafvb  32407  funopafvb  32408  afvco2  32427  fundmfibi  32632  usgfis  32764  usgfisALT  32768  4an31  33600  bj-seex  34838