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  6532  tposf2  6543  nnmordi  6793  nnmord  6794  nnaordex  6805  ectocld  6879  qsel  6890  mapsn  6976  f1oeng  7047  mapen  7150  nneneq  7162  findcard2  7197  findcard2s  7198  ac6sfi  7206  fiintim  7242  sbthlem1  7279  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  9756  zeo  9762  fnn0ind  9773  zindd  9775  btwnz  9776  lbzbi  10032  addmodlteq  10856  facwordi  11200  seq3coll  11316  ccatalpha  11403  pfxccatin12lem2a  11521  qdenre  11991  climcau  12138  serf0  12143  zsumdc  12176  fsum2dlemstep  12226  fsum2d  12227  fsumabs  12257  fsumiun  12269  zproddc  12371  fprod2dlemstep  12414  fprod2d  12415  odd2np1  12665  ndvdssub  12722  bitsinv1lem  12753  dfgcd2  12816  nprm  12926  rpexp  12957  pc2dvds  13138  pcfac  13158  4sqlem12  13210  4sqlem17  13215  prmlem0  13249  divsfval  13708  mulgaddcom  14008  mulginvcom  14009  cntz2ss  14168  gsumsnfdcmn  14257  ringinvnz1ne0  14461  lmss  15472  lmtopcnp  15476  txcn  15501  txlm  15505  xmettri2  15587  blin2  15658  metcnp3  15737  limcresi  15892  dvmptfsum  15951  sineq0re  16076  logbgcd1irr  16203  lgsdir2lem2  16353  lgsne0  16362  2lgsoddprm  16437  2sqlem6  16444  2sqlem10  16449  uhgr0vb  16530  wlk1walkdom  16805  wlkv0  16815  wlklenvclwlk  16819  bj-stim  16979  bj-stan  16980  bj-stand  16981  bj-stal  16982  bj-sbimedh  17004  bj-vtoclgft  17008  elabgft1  17011  elabgf2  17013