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  650  pm2.36  805  pm4.72  828  pm2.18dc  856  con1dc  857  jadc  864  pm2.521dcALT  871  con1biimdc  874  condandc  882  pm5.18dc  884  pm2.68dc  895  syl3an2  1283  syl2an23an  1310  xor3dc  1398  alrimdh  1490  spsd  1549  a5i  1554  19.21h  1568  hbnt  1664  hbae  1729  sbiedh  1798  exdistrfor  1811  sbcof2  1821  ax11a2  1832  ax11v  1838  sb4  1843  hbsb4t  2029  exmoeudc  2105  euimmo  2109  mopick  2120  r19.37  2646  spcimgft  2837  spcimegft  2839  rr19.28v  2901  mob2  2941  euind  2948  reuind  2966  sbeqalb  3043  triun  4141  csbexga  4158  copsexg  4274  trssord  4412  trsuc  4454  trsucss  4455  abnexg  4478  ralxfrd  4494  rexxfrd  4495  ralxfrALT  4499  sucprcreg  4582  nlimsucg  4599  tfis  4616  relssres  4981  issref  5049  dmsnopg  5138  dfco2a  5167  imadif  5335  fvelima  5609  mptfvex  5644  fvmptdf  5646  fvmptf  5651  funfvima2  5792  funfvima3  5793  foco2  5797  isores3  5859  oprabid  5951  ovmpt4g  6042  ovmpos  6043  ov2gf  6044  ovmpodf  6051  suppssfv  6128  suppssov1  6129  fo2ndf  6282  rntpos  6312  tposf2  6323  nnmordi  6571  nnmord  6572  nnaordex  6583  ectocld  6657  qsel  6668  mapsn  6746  f1oeng  6813  mapen  6904  nneneq  6915  findcard2  6947  findcard2s  6948  ac6sfi  6956  fiintim  6987  sbthlem1  7018  pr2ne  7254  ltbtwnnqq  7477  prnmaddl  7552  genpcdl  7581  genpcuu  7582  ltaddpr  7659  lteupri  7679  recexprlemss1l  7697  recexprlemss1u  7698  cauappcvgprlemdisj  7713  lttrsr  7824  recexgt0sr  7835  mulgt0sr  7840  axprecex  7942  rereceu  7951  addlsub  8391  recexap  8674  0mnnnnn0  9275  prime  9419  zeo  9425  fnn0ind  9436  zindd  9438  btwnz  9439  lbzbi  9684  addmodlteq  10472  facwordi  10814  seq3coll  10916  qdenre  11349  climcau  11493  serf0  11498  zsumdc  11530  fsum2dlemstep  11580  fsum2d  11581  fsumabs  11611  fsumiun  11623  zproddc  11725  fprod2dlemstep  11768  fprod2d  11769  odd2np1  12017  ndvdssub  12074  dfgcd2  12154  nprm  12264  rpexp  12294  pc2dvds  12471  pcfac  12491  4sqlem12  12543  4sqlem17  12548  divsfval  12914  mulgaddcom  13219  mulginvcom  13220  ringinvnz1ne0  13548  lmss  14425  lmtopcnp  14429  txcn  14454  txlm  14458  xmettri2  14540  blin2  14611  metcnp3  14690  limcresi  14845  dvmptfsum  14904  logbgcd1irr  15140  lgsdir2lem2  15186  lgsne0  15195  2lgsoddprm  15270  2sqlem6  15277  2sqlem10  15282  bj-stim  15308  bj-stan  15309  bj-stand  15310  bj-stal  15311  bj-sbimedh  15333  bj-vtoclgft  15337  elabgft1  15340  elabgf2  15342