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  4242  csbexga  4261  copsexg  4384  trssord  4525  trsuc  4567  trsucss  4568  abnexg  4592  ralxfrd  4608  rexxfrd  4609  ralxfrALT  4613  sucprcreg  4696  nlimsucg  4713  tfis  4730  relssres  5101  issref  5170  dmsnopg  5259  dfco2a  5288  imadif  5461  fvelima  5754  mptfvex  5791  fvmptdf  5793  fvmptf  5798  funfvima2  5951  funfvima3  5952  foco2  5959  isores3  6021  oprabid  6117  ovmpt4g  6211  ovmpos  6212  ov2gf  6213  ovmpodf  6220  suppssov1  6299  fo2ndf  6463  suppssfvg  6503  rntpos  6528  tposf2  6539  nnmordi  6789  nnmord  6790  nnaordex  6801  ectocld  6875  qsel  6886  mapsn  6972  f1oeng  7043  mapen  7146  nneneq  7158  findcard2  7193  findcard2s  7194  ac6sfi  7202  fiintim  7238  sbthlem1  7274  pr2ne  7539  ltbtwnnqq  7783  prnmaddl  7858  genpcdl  7887  genpcuu  7888  ltaddpr  7965  lteupri  7985  recexprlemss1l  8003  recexprlemss1u  8004  cauappcvgprlemdisj  8019  lttrsr  8130  recexgt0sr  8141  mulgt0sr  8146  axprecex  8248  rereceu  8257  addlsub  8698  recexap  8984  0mnnnnn0  9600  prime  9750  zeo  9756  fnn0ind  9767  zindd  9769  btwnz  9770  lbzbi  10026  addmodlteq  10850  facwordi  11194  seq3coll  11310  ccatalpha  11397  pfxccatin12lem2a  11515  qdenre  11985  climcau  12132  serf0  12137  zsumdc  12170  fsum2dlemstep  12220  fsum2d  12221  fsumabs  12251  fsumiun  12263  zproddc  12365  fprod2dlemstep  12408  fprod2d  12409  odd2np1  12659  ndvdssub  12716  bitsinv1lem  12747  dfgcd2  12810  nprm  12920  rpexp  12951  pc2dvds  13132  pcfac  13152  4sqlem12  13204  4sqlem17  13209  prmlem0  13243  divsfval  13702  mulgaddcom  14002  mulginvcom  14003  cntz2ss  14162  ringinvnz1ne0  14438  lmss  15438  lmtopcnp  15442  txcn  15467  txlm  15471  xmettri2  15553  blin2  15624  metcnp3  15703  limcresi  15858  dvmptfsum  15917  logbgcd1irr  16164  lgsdir2lem2  16314  lgsne0  16323  2lgsoddprm  16398  2sqlem6  16405  2sqlem10  16410  uhgr0vb  16491  wlk1walkdom  16766  wlkv0  16776  wlklenvclwlk  16780  bj-stim  16940  bj-stan  16941  bj-stand  16942  bj-stal  16943  bj-sbimedh  16965  bj-vtoclgft  16969  elabgft1  16972  elabgf2  16974