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  100  biimtrid  152  biimtrrid  153  imbitrid  154  adantld  278  adantrd  279  impel  280  mpan9  281  nsyli  652  pm2.36  809  pm4.72  832  pm2.18dc  860  con1dc  861  jadc  868  pm2.521dcALT  875  con1biimdc  878  condandc  886  pm5.18dc  888  pm2.68dc  899  syl3an2  1305  syl2an23an  1333  xor3dc  1429  alrimdh  1525  spsd  1584  a5i  1589  19.21h  1603  hbnt  1699  hbae  1764  sbiedh  1833  exdistrfor  1846  sbcof2  1856  ax11a2  1867  ax11v  1873  sb4  1878  hbsb4t  2064  exmoeudc  2141  euimmo  2145  mopick  2156  r19.37  2683  spcimgft  2879  spcimegft  2881  rr19.28v  2943  mob2  2983  euind  2990  reuind  3008  sbeqalb  3085  triun  4195  csbexga  4212  copsexg  4330  trssord  4471  trsuc  4513  trsucss  4514  abnexg  4537  ralxfrd  4553  rexxfrd  4554  ralxfrALT  4558  sucprcreg  4641  nlimsucg  4658  tfis  4675  relssres  5043  issref  5111  dmsnopg  5200  dfco2a  5229  imadif  5401  fvelima  5687  mptfvex  5722  fvmptdf  5724  fvmptf  5729  funfvima2  5876  funfvima3  5877  foco2  5883  isores3  5945  oprabid  6039  ovmpt4g  6133  ovmpos  6134  ov2gf  6135  ovmpodf  6142  suppssfv  6220  suppssov1  6221  fo2ndf  6379  rntpos  6409  tposf2  6420  nnmordi  6670  nnmord  6671  nnaordex  6682  ectocld  6756  qsel  6767  mapsn  6845  f1oeng  6916  mapen  7015  nneneq  7026  findcard2  7059  findcard2s  7060  ac6sfi  7068  fiintim  7101  sbthlem1  7132  pr2ne  7373  ltbtwnnqq  7610  prnmaddl  7685  genpcdl  7714  genpcuu  7715  ltaddpr  7792  lteupri  7812  recexprlemss1l  7830  recexprlemss1u  7831  cauappcvgprlemdisj  7846  lttrsr  7957  recexgt0sr  7968  mulgt0sr  7973  axprecex  8075  rereceu  8084  addlsub  8524  recexap  8808  0mnnnnn0  9409  prime  9554  zeo  9560  fnn0ind  9571  zindd  9573  btwnz  9574  lbzbi  9819  addmodlteq  10628  facwordi  10970  seq3coll  11072  pfxccatin12lem2a  11267  qdenre  11721  climcau  11866  serf0  11871  zsumdc  11903  fsum2dlemstep  11953  fsum2d  11954  fsumabs  11984  fsumiun  11996  zproddc  12098  fprod2dlemstep  12141  fprod2d  12142  odd2np1  12392  ndvdssub  12449  bitsinv1lem  12480  dfgcd2  12543  nprm  12653  rpexp  12683  pc2dvds  12861  pcfac  12881  4sqlem12  12933  4sqlem17  12938  divsfval  13369  mulgaddcom  13691  mulginvcom  13692  ringinvnz1ne0  14020  lmss  14928  lmtopcnp  14932  txcn  14957  txlm  14961  xmettri2  15043  blin2  15114  metcnp3  15193  limcresi  15348  dvmptfsum  15407  logbgcd1irr  15649  lgsdir2lem2  15716  lgsne0  15725  2lgsoddprm  15800  2sqlem6  15807  2sqlem10  15812  uhgr0vb  15892  wlk1walkdom  16080  wlkv0  16090  wlklenvclwlk  16094  bj-stim  16134  bj-stan  16135  bj-stand  16136  bj-stal  16137  bj-sbimedh  16159  bj-vtoclgft  16163  elabgft1  16166  elabgf2  16168