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  649  pm2.36  804  pm4.72  827  pm2.18dc  855  con1dc  856  jadc  863  pm2.521dcALT  870  con1biimdc  873  condandc  881  pm5.18dc  883  pm2.68dc  894  annimdc  937  syl3an2  1272  syl2an23an  1299  xor3dc  1387  alrimdh  1479  spsd  1538  a5i  1543  19.21h  1557  hbnt  1653  hbae  1718  sbiedh  1787  exdistrfor  1800  sbcof2  1810  ax11a2  1821  ax11v  1827  sb4  1832  hbsb4t  2013  exmoeudc  2089  euimmo  2093  mopick  2104  r19.37  2629  spcimgft  2815  spcimegft  2817  rr19.28v  2879  mob2  2919  euind  2926  reuind  2944  sbeqalb  3021  triun  4116  csbexga  4133  copsexg  4246  trssord  4382  trsuc  4424  trsucss  4425  abnexg  4448  ralxfrd  4464  rexxfrd  4465  ralxfrALT  4469  sucprcreg  4550  nlimsucg  4567  tfis  4584  relssres  4947  issref  5013  dmsnopg  5102  dfco2a  5131  imadif  5298  fvelima  5570  mptfvex  5604  fvmptdf  5606  fvmptf  5611  funfvima2  5752  funfvima3  5753  foco2  5757  isores3  5819  oprabid  5910  ovmpt4g  6000  ovmpos  6001  ov2gf  6002  ovmpodf  6009  suppssfv  6082  suppssov1  6083  fo2ndf  6231  rntpos  6261  tposf2  6272  nnmordi  6520  nnmord  6521  nnaordex  6532  ectocld  6604  qsel  6615  mapsn  6693  f1oeng  6760  mapen  6849  nneneq  6860  findcard2  6892  findcard2s  6893  ac6sfi  6901  fiintim  6931  sbthlem1  6959  pr2ne  7194  ltbtwnnqq  7417  prnmaddl  7492  genpcdl  7521  genpcuu  7522  ltaddpr  7599  lteupri  7619  recexprlemss1l  7637  recexprlemss1u  7638  cauappcvgprlemdisj  7653  lttrsr  7764  recexgt0sr  7775  mulgt0sr  7780  axprecex  7882  rereceu  7891  addlsub  8330  recexap  8613  0mnnnnn0  9211  prime  9355  zeo  9361  fnn0ind  9372  zindd  9374  btwnz  9375  lbzbi  9619  addmodlteq  10401  facwordi  10723  seq3coll  10825  qdenre  11214  climcau  11358  serf0  11363  zsumdc  11395  fsum2dlemstep  11445  fsum2d  11446  fsumabs  11476  fsumiun  11488  zproddc  11590  fprod2dlemstep  11633  fprod2d  11634  odd2np1  11881  ndvdssub  11938  dfgcd2  12018  nprm  12126  rpexp  12156  pc2dvds  12332  pcfac  12351  mulgaddcom  13017  mulginvcom  13018  ringinvnz1ne0  13237  lmss  13907  lmtopcnp  13911  txcn  13936  txlm  13940  xmettri2  14022  blin2  14093  metcnp3  14172  limcresi  14296  logbgcd1irr  14546  lgsdir2lem2  14591  lgsne0  14600  2sqlem6  14628  2sqlem10  14633  bj-stim  14659  bj-stan  14660  bj-stand  14661  bj-stal  14662  bj-sbimedh  14684  bj-vtoclgft  14688  elabgft1  14691  elabgf2  14693