Theorem syl5 28

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	⊢ (𝜑 → 𝜓)
syl5.2	⊢ (𝜒 → (𝜓 → 𝜃))

Assertion

Ref	Expression
syl5	⊢ (𝜒 → (𝜑 → 𝜃))

Proof of Theorem syl5

Step	Hyp	Ref	Expression
1		syl5.1	. . 3 ⊢ (𝜑 → 𝜓)
2		syl5.2	. . 3 ⊢ (𝜒 → (𝜓 → 𝜃))
3	1, 2	syl5com 26	. 2 ⊢ (𝜑 → (𝜒 → 𝜃))
4	3	com12 27	1 ⊢ (𝜒 → (𝜑 → 𝜃))

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  30  syl2im  34  imim12i  53  pm2.86d  93  syl5bi  141  syl5bir  142  syl5ib  143  adantld  263  adantrd  264  mpan9  265  nsyli  578  pm2.36  717  pm4.72  736  pm2.18dc  750  con1dc  753  jadc  760  pm2.521dc  764  con1biimdc  767  condandc  775  pm5.18dc  777  pm2.68dc  793  annimdc  845  syl3an2  1169  xor3dc  1278  alrimdh  1368  spsd  1431  a5i  1435  19.21h  1449  hbnt  1543  hbae  1606  sbiedh  1670  exdistrfor  1681  sbcof2  1691  ax11a2  1702  ax11v  1708  sb4  1713  hbsb4t  1889  exmoeudc  1963  euimmo  1967  mopick  1978  r19.37  2462  spcimgft  2629  spcimegft  2631  rr19.28v  2683  mob2  2721  euind  2728  reuind  2744  sbeqalb  2815  sbcimdv  2823  triun  3867  csbexga  3885  copsexg  3981  trssord  4117  trsuc  4159  trsucss  4160  ralxfrd  4194  rexxfrd  4195  ralxfrALT  4199  sucprcreg  4273  nlimsucg  4290  tfis  4306  relssres  4648  issref  4707  dmsnopg  4792  dfco2a  4821  imadif  4979  fvelima  5225  mptfvex  5256  fvmptdf  5258  fvmptf  5263  foco2  5318  funfvima2  5391  funfvima3  5392  isores3  5455  oprabid  5537  ovmpt4g  5623  ovmpt2s  5624  ov2gf  5625  ovmpt2df  5632  suppssfv  5708  suppssov1  5709  fo2ndf  5848  rntpos  5872  tposf2  5883  nnmordi  6089  nnmord  6090  nnaordex  6100  ectocld  6172  qsel  6183  f1oeng  6237  nneneq  6320  findcard2  6346  findcard2s  6347  ac6sfi  6352  ltbtwnnqq  6513  prnmaddl  6588  genpcdl  6617  genpcuu  6618  ltaddpr  6695  lteupri  6715  recexprlemss1l  6733  recexprlemss1u  6734  cauappcvgprlemdisj  6749  lttrsr  6847  recexgt0sr  6858  mulgt0sr  6862  axprecex  6954  rereceu  6963  recexap  7634  0mnnnnn0  8214  prime  8337  zeo  8343  fnn0ind  8354  zindd  8356  btwnz  8357  lbzbi  8551  qdenre  9798  climcau  9866  serif0  9871  bj-sbimedh  9911  bj-vtoclgft  9914  elabgft1  9917  elabgf2  9919