Theorem syl5 32

Description: A syllogism rule of inference. The second premise is used to replace the second antecedent of the first premise. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 25-May-2013.)

Hypotheses

Ref	Expression
syl5.1	|- ( ph -> ps )
syl5.2	|- ( ch -> ( ps -> th ) )

Assertion

Ref	Expression
syl5	|- ( ch -> ( ph -> th ) )

Proof of Theorem syl5

Step	Hyp	Ref	Expression
1		syl5.1	. . 3 |- ( ph -> ps )
2		syl5.2	. . 3 |- ( ch -> ( ps -> th ) )
3	1, 2	syl5com 29	. 2 |- ( ph -> ( ch -> th ) )
4	3	com12 30	1 |- ( ch -> ( ph -> th ) )

Syntax hints:   -> wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is referenced by:  syl56  34  syl2im  38  imim12i  59  pm2.86d  100  biimtrid  152  biimtrrid  153  imbitrid  154  adantld  278  adantrd  279  impel  280  mpan9  281  nsyli  652  pm2.36  809  pm4.72  832  pm2.18dc  860  con1dc  861  jadc  868  pm2.521dcALT  875  con1biimdc  878  condandc  886  pm5.18dc  888  pm2.68dc  899  syl3an2  1305  syl2an23an  1333  xor3dc  1429  alrimdh  1525  spsd  1584  a5i  1589  19.21h  1603  hbnt  1699  hbae  1764  sbiedh  1833  exdistrfor  1846  sbcof2  1856  ax11a2  1867  ax11v  1873  sb4  1878  hbsb4t  2064  exmoeudc  2141  euimmo  2145  mopick  2156  r19.37  2683  spcimgft  2879  spcimegft  2881  rr19.28v  2943  mob2  2983  euind  2990  reuind  3008  sbeqalb  3085  triun  4195  csbexga  4212  copsexg  4330  trssord  4471  trsuc  4513  trsucss  4514  abnexg  4537  ralxfrd  4553  rexxfrd  4554  ralxfrALT  4558  sucprcreg  4641  nlimsucg  4658  tfis  4675  relssres  5043  issref  5111  dmsnopg  5200  dfco2a  5229  imadif  5401  fvelima  5687  mptfvex  5722  fvmptdf  5724  fvmptf  5729  funfvima2  5876  funfvima3  5877  foco2  5883  isores3  5945  oprabid  6039  ovmpt4g  6133  ovmpos  6134  ov2gf  6135  ovmpodf  6142  suppssfv  6220  suppssov1  6221  fo2ndf  6379  rntpos  6409  tposf2  6420  nnmordi  6670  nnmord  6671  nnaordex  6682  ectocld  6756  qsel  6767  mapsn  6845  f1oeng  6916  mapen  7015  nneneq  7026  findcard2  7059  findcard2s  7060  ac6sfi  7068  fiintim  7104  sbthlem1  7135  pr2ne  7376  ltbtwnnqq  7613  prnmaddl  7688  genpcdl  7717  genpcuu  7718  ltaddpr  7795  lteupri  7815  recexprlemss1l  7833  recexprlemss1u  7834  cauappcvgprlemdisj  7849  lttrsr  7960  recexgt0sr  7971  mulgt0sr  7976  axprecex  8078  rereceu  8087  addlsub  8527  recexap  8811  0mnnnnn0  9412  prime  9557  zeo  9563  fnn0ind  9574  zindd  9576  btwnz  9577  lbzbi  9823  addmodlteq  10632  facwordi  10974  seq3coll  11077  ccatalpha  11161  pfxccatin12lem2a  11275  qdenre  11729  climcau  11874  serf0  11879  zsumdc  11911  fsum2dlemstep  11961  fsum2d  11962  fsumabs  11992  fsumiun  12004  zproddc  12106  fprod2dlemstep  12149  fprod2d  12150  odd2np1  12400  ndvdssub  12457  bitsinv1lem  12488  dfgcd2  12551  nprm  12661  rpexp  12691  pc2dvds  12869  pcfac  12889  4sqlem12  12941  4sqlem17  12946  divsfval  13377  mulgaddcom  13699  mulginvcom  13700  ringinvnz1ne0  14028  lmss  14936  lmtopcnp  14940  txcn  14965  txlm  14969  xmettri2  15051  blin2  15122  metcnp3  15201  limcresi  15356  dvmptfsum  15415  logbgcd1irr  15657  lgsdir2lem2  15724  lgsne0  15733  2lgsoddprm  15808  2sqlem6  15815  2sqlem10  15820  uhgr0vb  15900  wlk1walkdom  16105  wlkv0  16115  wlklenvclwlk  16119  bj-stim  16193  bj-stan  16194  bj-stand  16195  bj-stal  16196  bj-sbimedh  16218  bj-vtoclgft  16222  elabgft1  16225  elabgf2  16227