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  654  pm2.36  812  pm4.72  835  pm2.18dc  863  con1dc  864  jadc  871  pm2.521dcALT  878  con1biimdc  881  condandc  889  pm5.18dc  891  pm2.68dc  902  syl3an2  1308  syl2an23an  1336  xor3dc  1432  alrimdh  1528  spsd  1587  a5i  1592  19.21h  1606  hbnt  1701  hbae  1766  sbiedh  1835  exdistrfor  1848  sbcof2  1858  ax11a2  1869  ax11v  1875  sb4  1880  hbsb4t  2066  exmoeudc  2143  euimmo  2147  mopick  2158  r19.37  2686  spcimgft  2883  spcimegft  2885  rr19.28v  2947  mob2  2987  euind  2994  reuind  3012  sbeqalb  3089  triun  4205  csbexga  4222  copsexg  4342  trssord  4483  trsuc  4525  trsucss  4526  abnexg  4549  ralxfrd  4565  rexxfrd  4566  ralxfrALT  4570  sucprcreg  4653  nlimsucg  4670  tfis  4687  relssres  5057  issref  5126  dmsnopg  5215  dfco2a  5244  imadif  5417  fvelima  5706  mptfvex  5741  fvmptdf  5743  fvmptf  5748  funfvima2  5897  funfvima3  5898  foco2  5904  isores3  5966  oprabid  6060  ovmpt4g  6154  ovmpos  6155  ov2gf  6156  ovmpodf  6163  suppssov1  6241  fo2ndf  6401  suppssfvg  6441  rntpos  6466  tposf2  6477  nnmordi  6727  nnmord  6728  nnaordex  6739  ectocld  6813  qsel  6824  mapsn  6902  f1oeng  6973  mapen  7075  nneneq  7086  findcard2  7121  findcard2s  7122  ac6sfi  7130  fiintim  7166  sbthlem1  7199  pr2ne  7440  ltbtwnnqq  7678  prnmaddl  7753  genpcdl  7782  genpcuu  7783  ltaddpr  7860  lteupri  7880  recexprlemss1l  7898  recexprlemss1u  7899  cauappcvgprlemdisj  7914  lttrsr  8025  recexgt0sr  8036  mulgt0sr  8041  axprecex  8143  rereceu  8152  addlsub  8591  recexap  8875  0mnnnnn0  9476  prime  9623  zeo  9629  fnn0ind  9640  zindd  9642  btwnz  9643  lbzbi  9894  addmodlteq  10706  facwordi  11048  seq3coll  11152  ccatalpha  11239  pfxccatin12lem2a  11357  qdenre  11825  climcau  11970  serf0  11975  zsumdc  12008  fsum2dlemstep  12058  fsum2d  12059  fsumabs  12089  fsumiun  12101  zproddc  12203  fprod2dlemstep  12246  fprod2d  12247  odd2np1  12497  ndvdssub  12554  bitsinv1lem  12585  dfgcd2  12648  nprm  12758  rpexp  12788  pc2dvds  12966  pcfac  12986  4sqlem12  13038  4sqlem17  13043  divsfval  13474  mulgaddcom  13796  mulginvcom  13797  ringinvnz1ne0  14126  lmss  15040  lmtopcnp  15044  txcn  15069  txlm  15073  xmettri2  15155  blin2  15226  metcnp3  15305  limcresi  15460  dvmptfsum  15519  logbgcd1irr  15761  lgsdir2lem2  15831  lgsne0  15840  2lgsoddprm  15915  2sqlem6  15922  2sqlem10  15927  uhgr0vb  16008  wlk1walkdom  16283  wlkv0  16293  wlklenvclwlk  16297  bj-stim  16447  bj-stan  16448  bj-stand  16449  bj-stal  16450  bj-sbimedh  16472  bj-vtoclgft  16476  elabgft1  16479  elabgf2  16481