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	⊢ (𝜑 → 𝜓)
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 29	. 2 ⊢ (𝜑 → (𝜒 → 𝜃))
4	3	com12 30	1 ⊢ (𝜒 → (𝜑 → 𝜃))

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  99  syl5bi  151  syl5bir  152  syl5ib  153  adantld  276  adantrd  277  impel  278  mpan9  279  nsyli  639  pm2.36  794  pm4.72  817  const  842  pm2.18dc  845  con1dc  846  jadc  853  pm2.521dcALT  860  con1biimdc  863  condandc  871  pm5.18dc  873  pm2.68dc  884  annimdc  926  syl3an2  1261  syl2an23an  1288  xor3dc  1376  alrimdh  1466  spsd  1525  a5i  1530  19.21h  1544  hbnt  1640  hbae  1705  sbiedh  1774  exdistrfor  1787  sbcof2  1797  ax11a2  1808  ax11v  1814  sb4  1819  hbsb4t  2000  exmoeudc  2076  euimmo  2080  mopick  2091  r19.37  2616  spcimgft  2797  spcimegft  2799  rr19.28v  2861  mob2  2901  euind  2908  reuind  2926  sbeqalb  3002  triun  4087  csbexga  4104  copsexg  4216  trssord  4352  trsuc  4394  trsucss  4395  abnexg  4418  ralxfrd  4434  rexxfrd  4435  ralxfrALT  4439  sucprcreg  4520  nlimsucg  4537  tfis  4554  relssres  4916  issref  4980  dmsnopg  5069  dfco2a  5098  imadif  5262  fvelima  5532  mptfvex  5565  fvmptdf  5567  fvmptf  5572  funfvima2  5711  funfvima3  5712  foco2  5716  isores3  5777  oprabid  5865  ovmpt4g  5955  ovmpos  5956  ov2gf  5957  ovmpodf  5964  suppssfv  6040  suppssov1  6041  fo2ndf  6186  rntpos  6216  tposf2  6227  nnmordi  6475  nnmord  6476  nnaordex  6486  ectocld  6558  qsel  6569  mapsn  6647  f1oeng  6714  mapen  6803  nneneq  6814  findcard2  6846  findcard2s  6847  ac6sfi  6855  fiintim  6885  sbthlem1  6913  pr2ne  7139  ltbtwnnqq  7347  prnmaddl  7422  genpcdl  7451  genpcuu  7452  ltaddpr  7529  lteupri  7549  recexprlemss1l  7567  recexprlemss1u  7568  cauappcvgprlemdisj  7583  lttrsr  7694  recexgt0sr  7705  mulgt0sr  7710  axprecex  7812  rereceu  7821  addlsub  8259  recexap  8541  0mnnnnn0  9137  prime  9281  zeo  9287  fnn0ind  9298  zindd  9300  btwnz  9301  lbzbi  9545  addmodlteq  10323  facwordi  10642  seq3coll  10741  qdenre  11130  climcau  11274  serf0  11279  zsumdc  11311  fsum2dlemstep  11361  fsum2d  11362  fsumabs  11392  fsumiun  11404  zproddc  11506  fprod2dlemstep  11549  fprod2d  11550  odd2np1  11795  ndvdssub  11852  dfgcd2  11932  nprm  12034  rpexp  12062  pc2dvds  12238  pcfac  12257  lmss  12787  lmtopcnp  12791  txcn  12816  txlm  12820  xmettri2  12902  blin2  12973  metcnp3  13052  limcresi  13176  logbgcd1irr  13426  bj-stim  13461  bj-stan  13462  bj-stand  13463  bj-stal  13464  bj-sbimedh  13487  bj-vtoclgft  13491  elabgft1  13494  elabgf2  13496