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 ) )

This proof depends on syntax axioms:   -> wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used 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  4244  csbexga  4263  copsexg  4386  trssord  4527  trsuc  4569  trsucss  4570  abnexg  4594  ralxfrd  4610  rexxfrd  4611  ralxfrALT  4615  sucprcreg  4698  nlimsucg  4715  tfis  4732  relssres  5103  issref  5173  dmsnopg  5262  dfco2a  5291  imadif  5464  fvelima  5757  mptfvex  5794  fvmptdf  5796  fvmptf  5801  funfvima2  5954  funfvima3  5955  foco2  5962  isores3  6024  oprabid  6120  ovmpt4g  6214  ovmpos  6215  ov2gf  6216  ovmpodf  6223  suppssov1  6302  fo2ndf  6467  suppssfvg  6507  rntpos  6533  tposf2  6544  nnmordi  6794  nnmord  6795  nnaordex  6806  ectocld  6880  qsel  6891  mapsn  6978  f1oeng  7049  mapen  7152  nneneq  7164  findcard2  7199  findcard2s  7200  ac6sfi  7208  fiintim  7244  sbthlem1  7281  pr2ne  7544  ltbtwnnqq  7788  prnmaddl  7863  genpcdl  7892  genpcuu  7893  ltaddpr  7970  lteupri  7990  recexprlemss1l  8008  recexprlemss1u  8009  cauappcvgprlemdisj  8024  lttrsr  8135  recexgt0sr  8146  mulgt0sr  8151  axprecex  8253  rereceu  8262  addlsub  8703  recexap  8989  0mnnnnn0  9606  prime  9755  zeo  9761  fnn0ind  9772  zindd  9774  btwnz  9775  lbzbi  10031  addmodlteq  10855  facwordi  11199  seq3coll  11315  ccatalpha  11402  pfxccatin12lem2a  11520  qdenre  11990  climcau  12137  serf0  12142  zsumdc  12175  fsum2dlemstep  12225  fsum2d  12226  fsumabs  12256  fsumiun  12268  zproddc  12370  fprod2dlemstep  12413  fprod2d  12414  odd2np1  12664  ndvdssub  12721  bitsinv1lem  12752  dfgcd2  12815  nprm  12925  rpexp  12956  pc2dvds  13137  pcfac  13157  4sqlem12  13209  4sqlem17  13214  prmlem0  13248  divsfval  13707  mulgaddcom  14007  mulginvcom  14008  cntz2ss  14167  gsumsnfdcmn  14256  ringinvnz1ne0  14460  lmss  15489  lmtopcnp  15493  txcn  15518  txlm  15522  xmettri2  15604  blin2  15675  metcnp3  15754  limcresi  15909  dvmptfsum  15968  sineq0re  16093  logbgcd1irr  16220  lgsdir2lem2  16370  lgsne0  16379  2lgsoddprm  16454  2sqlem6  16461  2sqlem10  16466  uhgr0vb  16547  wlk1walkdom  16822  wlkv0  16832  wlklenvclwlk  16836  bj-stim  16996  bj-stan  16997  bj-stand  16998  bj-stal  16999  bj-sbimedh  17021  bj-vtoclgft  17025  elabgft1  17028  elabgf2  17030