Theorem sylanb 469

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 468	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  476  anabsan  804  eqtr2  2459  pm13.181  2682  rmob  3283  sspsstr  3458  disjne  3721  seex  4679  tron  4738  xpcan2  5272  fssres  5575  funbrfvb  5731  funopfvb  5732  fvco  5764  fvimacnvi  5814  ffvresb  5871  funressn  5892  funresdfunsn  5917  fvtp2  5923  fvtp2g  5926  fnex  5941  funex  5942  ordsucss  6428  ordsucelsuc  6432  1st2nd  6619  frxp  6681  dftpos4  6763  tz7.48lem  6892  nnmsucr  7060  nnmcan  7069  xpmapenlem  7474  php  7491  php4  7494  omsucdomOLD  7502  isfinite2  7566  wofib  7755  r1limg  7974  r1pwcl  8050  cardmin2  8164  zornn0g  8670  intgru  8977  supsrlem  9274  uzindOLD  10732  fnn0ind  10737  uztrn2  10874  nnwo  10916  irradd  10973  qbtwnxr  11166  xltnegi  11182  xaddnemnf  11200  xaddnepnf  11201  xaddcom  11204  xnegdi  11207  elioore  11326  uzsubsubfz1  11468  fzo1fzo0n0  11584  elfzonelfzo  11623  leexp2  11914  faclbnd  12062  faclbnd3  12064  brfi1uzind  12215  swrdccat3b  12383  dvdslelem  13573  divalglem1  13594  isprm2lem  13766  dvdsprime  13772  pcgcd  13940  cntri  15841  efgsrel  16224  xrsdsreclb  17819  znf1o  17943  restuni  18725  stoig  18726  restperf  18747  resstps  18750  pnfnei  18783  mnfnei  18784  cnnei  18845  cmpsublem  18961  tx1stc  19182  xkopt  19187  isfcls  19541  tgioo  20332  opnreen  20367  iscmet3  20763  dyaddisj  21035  limcmpt  21317  degltlem1  21502  ulmdvlem3  21826  lgsdi  22630  eupath2lem3  23535  grpoidinvlem3  23628  ipasslem3  24168  spanuni  24882  5oalem3  24994  5oalem5  24996  mdslmd1lem2  25665  mptct  25953  mptctf  25956  xaddeq0  25981  ordtconlem1  26290  esumcvg  26471  measres  26572  measdivcstOLD  26574  measdivcst  26575  probun  26732  dfon2lem9  27533  noreson  27730  funpartfun  27903  cgrxfr  28015  segcon2  28065  brsegle2  28069  seglecgr12im  28070  segletr  28074  ftc1anclem5  28396  ftc1anc  28400  nn0prpw  28443  comppfsc  28504  exlimddvfi  28855  prtlem11  28936  mzpclall  28988  funbrafvb  29987  funopafvb  29988  afvco2  30007  2wlkonotv  30321  clwlkfclwwlk  30442  dmatsubcl  30760  bj-seex  32160