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  4194  csbexga  4211  copsexg  4329  trssord  4468  trsuc  4510  trsucss  4511  abnexg  4534  ralxfrd  4550  rexxfrd  4551  ralxfrALT  4555  sucprcreg  4638  nlimsucg  4655  tfis  4672  relssres  5039  issref  5107  dmsnopg  5196  dfco2a  5225  imadif  5397  fvelima  5678  mptfvex  5713  fvmptdf  5715  fvmptf  5720  funfvima2  5865  funfvima3  5866  foco2  5870  isores3  5932  oprabid  6026  ovmpt4g  6118  ovmpos  6119  ov2gf  6120  ovmpodf  6127  suppssfv  6204  suppssov1  6205  fo2ndf  6363  rntpos  6393  tposf2  6404  nnmordi  6652  nnmord  6653  nnaordex  6664  ectocld  6738  qsel  6749  mapsn  6827  f1oeng  6898  mapen  6995  nneneq  7006  findcard2  7039  findcard2s  7040  ac6sfi  7048  fiintim  7081  sbthlem1  7112  pr2ne  7353  ltbtwnnqq  7590  prnmaddl  7665  genpcdl  7694  genpcuu  7695  ltaddpr  7772  lteupri  7792  recexprlemss1l  7810  recexprlemss1u  7811  cauappcvgprlemdisj  7826  lttrsr  7937  recexgt0sr  7948  mulgt0sr  7953  axprecex  8055  rereceu  8064  addlsub  8504  recexap  8788  0mnnnnn0  9389  prime  9534  zeo  9540  fnn0ind  9551  zindd  9553  btwnz  9554  lbzbi  9799  addmodlteq  10607  facwordi  10949  seq3coll  11051  pfxccatin12lem2a  11245  qdenre  11699  climcau  11844  serf0  11849  zsumdc  11881  fsum2dlemstep  11931  fsum2d  11932  fsumabs  11962  fsumiun  11974  zproddc  12076  fprod2dlemstep  12119  fprod2d  12120  odd2np1  12370  ndvdssub  12427  bitsinv1lem  12458  dfgcd2  12521  nprm  12631  rpexp  12661  pc2dvds  12839  pcfac  12859  4sqlem12  12911  4sqlem17  12916  divsfval  13347  mulgaddcom  13669  mulginvcom  13670  ringinvnz1ne0  13998  lmss  14905  lmtopcnp  14909  txcn  14934  txlm  14938  xmettri2  15020  blin2  15091  metcnp3  15170  limcresi  15325  dvmptfsum  15384  logbgcd1irr  15626  lgsdir2lem2  15693  lgsne0  15702  2lgsoddprm  15777  2sqlem6  15784  2sqlem10  15789  uhgr0vb  15869  bj-stim  16040  bj-stan  16041  bj-stand  16042  bj-stal  16043  bj-sbimedh  16065  bj-vtoclgft  16069  elabgft1  16072  elabgf2  16074