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  658  pm2.36  816  pm4.72  839  pm2.18dc  867  con1dc  868  jadc  875  pm2.521dcALT  882  con1biimdc  885  condandc  893  pm5.18dc  895  pm2.68dc  906  syl3an2  1312  syl2an23an  1340  xor3dc  1436  alrimdh  1532  spsd  1591  a5i  1596  19.21h  1610  hbnt  1705  hbae  1770  sbiedh  1840  exdistrfor  1853  sbcof2  1863  ax11a2  1874  ax11v  1880  sb4  1885  hbsb4t  2073  exmoeudc  2150  euimmo  2154  mopick  2165  r19.37  2703  spcimgft  2901  spcimegft  2903  rr19.28v  2966  mob2  3006  euind  3013  reuind  3031  sbeqalb  3108  triun  4237  csbexga  4256  copsexg  4379  trssord  4520  trsuc  4562  trsucss  4563  abnexg  4587  ralxfrd  4603  rexxfrd  4604  ralxfrALT  4608  sucprcreg  4691  nlimsucg  4708  tfis  4725  relssres  5096  issref  5165  dmsnopg  5254  dfco2a  5283  imadif  5456  fvelima  5748  mptfvex  5785  fvmptdf  5787  fvmptf  5792  funfvima2  5941  funfvima3  5942  foco2  5949  isores3  6011  oprabid  6107  ovmpt4g  6201  ovmpos  6202  ov2gf  6203  ovmpodf  6210  suppssov1  6289  fo2ndf  6453  suppssfvg  6493  rntpos  6518  tposf2  6529  nnmordi  6779  nnmord  6780  nnaordex  6791  ectocld  6865  qsel  6876  mapsn  6962  f1oeng  7033  mapen  7136  nneneq  7148  findcard2  7183  findcard2s  7184  ac6sfi  7192  fiintim  7228  sbthlem1  7264  pr2ne  7528  ltbtwnnqq  7772  prnmaddl  7847  genpcdl  7876  genpcuu  7877  ltaddpr  7954  lteupri  7974  recexprlemss1l  7992  recexprlemss1u  7993  cauappcvgprlemdisj  8008  lttrsr  8119  recexgt0sr  8130  mulgt0sr  8135  axprecex  8237  rereceu  8246  addlsub  8686  recexap  8971  0mnnnnn0  9574  prime  9724  zeo  9730  fnn0ind  9741  zindd  9743  btwnz  9744  lbzbi  9995  addmodlteq  10813  facwordi  11156  seq3coll  11272  ccatalpha  11359  pfxccatin12lem2a  11477  qdenre  11946  climcau  12091  serf0  12096  zsumdc  12129  fsum2dlemstep  12179  fsum2d  12180  fsumabs  12210  fsumiun  12222  zproddc  12324  fprod2dlemstep  12367  fprod2d  12368  odd2np1  12618  ndvdssub  12675  bitsinv1lem  12706  dfgcd2  12769  nprm  12879  rpexp  12909  pc2dvds  13087  pcfac  13107  4sqlem12  13159  4sqlem17  13164  divsfval  13626  mulgaddcom  13926  mulginvcom  13927  ringinvnz1ne0  14327  lmss  15270  lmtopcnp  15274  txcn  15299  txlm  15303  xmettri2  15385  blin2  15456  metcnp3  15535  limcresi  15690  dvmptfsum  15749  logbgcd1irr  15992  lgsdir2lem2  16062  lgsne0  16071  2lgsoddprm  16146  2sqlem6  16153  2sqlem10  16158  uhgr0vb  16239  wlk1walkdom  16514  wlkv0  16524  wlklenvclwlk  16528  bj-stim  16688  bj-stan  16689  bj-stand  16690  bj-stal  16691  bj-sbimedh  16713  bj-vtoclgft  16717  elabgft1  16720  elabgf2  16722