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-1 5  ax-2 6  ax-mp 7

This theorem is referenced by:  syl56  34  syl2im  38  imim12i  59  pm2.86d  99  syl5bi  151  syl5bir  152  syl5ib  153  adantld  273  adantrd  274  impel  275  mpan9  276  nsyli  614  pm2.36  754  pm4.72  773  pm2.18dc  789  con1dc  792  jadc  799  pm2.521dc  803  con1biimdc  806  condandc  814  pm5.18dc  816  pm2.68dc  832  annimdc  884  syl3an2  1209  syl2an23an  1236  xor3dc  1324  alrimdh  1414  spsd  1477  a5i  1481  19.21h  1495  hbnt  1589  hbae  1654  sbiedh  1718  exdistrfor  1729  sbcof2  1739  ax11a2  1750  ax11v  1756  sb4  1761  hbsb4t  1938  exmoeudc  2012  euimmo  2016  mopick  2027  r19.37  2522  spcimgft  2698  spcimegft  2700  rr19.28v  2759  mob2  2798  euind  2805  reuind  2823  sbeqalb  2898  triun  3957  csbexga  3975  copsexg  4082  trssord  4218  trsuc  4260  trsucss  4261  abnexg  4283  ralxfrd  4299  rexxfrd  4300  ralxfrALT  4304  sucprcreg  4380  nlimsucg  4397  tfis  4413  relssres  4765  issref  4829  dmsnopg  4917  dfco2a  4946  imadif  5109  fvelima  5371  mptfvex  5403  fvmptdf  5405  fvmptf  5410  funfvima2  5543  funfvima3  5544  foco2  5549  isores3  5610  oprabid  5697  ovmpt4g  5783  ovmpt2s  5784  ov2gf  5785  ovmpt2df  5792  suppssfv  5868  suppssov1  5869  fo2ndf  6008  rntpos  6038  tposf2  6049  nnmordi  6291  nnmord  6292  nnaordex  6302  ectocld  6374  qsel  6385  mapsn  6463  f1oeng  6530  mapen  6618  nneneq  6629  findcard2  6661  findcard2s  6662  ac6sfi  6670  fiintim  6695  sbthlem1  6722  pr2ne  6883  ltbtwnnqq  7037  prnmaddl  7112  genpcdl  7141  genpcuu  7142  ltaddpr  7219  lteupri  7239  recexprlemss1l  7257  recexprlemss1u  7258  cauappcvgprlemdisj  7273  lttrsr  7371  recexgt0sr  7382  mulgt0sr  7386  axprecex  7478  rereceu  7487  addlsub  7911  recexap  8185  0mnnnnn0  8768  prime  8908  zeo  8914  fnn0ind  8925  zindd  8927  btwnz  8928  lbzbi  9164  addmodlteq  9868  facwordi  10211  iseqcoll  10310  qdenre  10698  climcau  10799  serf0  10804  zisum  10837  fsum2dlemstep  10891  fsum2d  10892  fsumabs  10922  fsumiun  10934  odd2np1  11214  ndvdssub  11271  dfgcd2  11344  nprm  11446  rpexp  11473  bj-sbimedh  11976  bj-vtoclgft  11979  elabgft1  11982  elabgf2  11984