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  58  pm2.86d  98  syl5bi  150  syl5bir  151  syl5ib  152  adantld  272  adantrd  273  impel  274  mpan9  275  nsyli  610  pm2.36  750  pm4.72  769  pm2.18dc  783  con1dc  786  jadc  793  pm2.521dc  797  con1biimdc  800  condandc  808  pm5.18dc  810  pm2.68dc  826  annimdc  878  syl3an2  1203  syl2an23an  1230  xor3dc  1318  alrimdh  1408  spsd  1471  a5i  1475  19.21h  1489  hbnt  1583  hbae  1646  sbiedh  1710  exdistrfor  1721  sbcof2  1731  ax11a2  1742  ax11v  1748  sb4  1753  hbsb4t  1930  exmoeudc  2004  euimmo  2008  mopick  2019  r19.37  2506  spcimgft  2674  spcimegft  2676  rr19.28v  2734  mob2  2772  euind  2779  reuind  2795  sbeqalb  2870  triun  3888  csbexga  3906  copsexg  3999  trssord  4135  trsuc  4177  trsucss  4178  ralxfrd  4212  rexxfrd  4213  ralxfrALT  4217  sucprcreg  4292  nlimsucg  4309  tfis  4324  relssres  4666  issref  4727  dmsnopg  4812  dfco2a  4841  imadif  4999  fvelima  5246  mptfvex  5277  fvmptdf  5279  fvmptf  5284  foco2  5339  funfvima2  5412  funfvima3  5413  isores3  5475  oprabid  5557  ovmpt4g  5643  ovmpt2s  5644  ov2gf  5645  ovmpt2df  5652  suppssfv  5728  suppssov1  5729  fo2ndf  5868  rntpos  5895  tposf2  5906  nnmordi  6112  nnmord  6113  nnaordex  6123  ectocld  6195  qsel  6206  f1oeng  6260  nneneq  6343  findcard2  6373  findcard2s  6374  ac6sfi  6379  pr2ne  6461  ltbtwnnqq  6605  prnmaddl  6680  genpcdl  6709  genpcuu  6710  ltaddpr  6787  lteupri  6807  recexprlemss1l  6825  recexprlemss1u  6826  cauappcvgprlemdisj  6841  lttrsr  6939  recexgt0sr  6950  mulgt0sr  6954  axprecex  7046  rereceu  7055  addlsub  7474  recexap  7743  0mnnnnn0  8320  prime  8446  zeo  8452  fnn0ind  8463  zindd  8465  btwnz  8466  lbzbi  8701  addmodlteq  9400  facwordi  9667  qdenre  10088  climcau  10184  serif0  10189  odd2np1  10272  ndvdssub  10330  dfgcd2  10403  nprm  10505  rpexp  10532  bj-sbimedh  10582  bj-vtoclgft  10585  elabgft1  10588  elabgf2  10590