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  654  pm2.36  812  pm4.72  835  pm2.18dc  863  con1dc  864  jadc  871  pm2.521dcALT  878  con1biimdc  881  condandc  889  pm5.18dc  891  pm2.68dc  902  syl3an2  1308  syl2an23an  1336  xor3dc  1432  alrimdh  1528  spsd  1587  a5i  1592  19.21h  1606  hbnt  1701  hbae  1766  sbiedh  1836  exdistrfor  1849  sbcof2  1859  ax11a2  1870  ax11v  1876  sb4  1881  hbsb4t  2067  exmoeudc  2144  euimmo  2148  mopick  2159  r19.37  2695  spcimgft  2892  spcimegft  2894  rr19.28v  2956  mob2  2996  euind  3003  reuind  3021  sbeqalb  3098  triun  4220  csbexga  4237  copsexg  4359  trssord  4500  trsuc  4542  trsucss  4543  abnexg  4566  ralxfrd  4582  rexxfrd  4583  ralxfrALT  4587  sucprcreg  4670  nlimsucg  4687  tfis  4704  relssres  5075  issref  5144  dmsnopg  5233  dfco2a  5262  imadif  5435  fvelima  5727  mptfvex  5762  fvmptdf  5764  fvmptf  5769  funfvima2  5918  funfvima3  5919  foco2  5925  isores3  5987  oprabid  6081  ovmpt4g  6175  ovmpos  6176  ov2gf  6177  ovmpodf  6184  suppssov1  6262  fo2ndf  6422  suppssfvg  6462  rntpos  6487  tposf2  6498  nnmordi  6748  nnmord  6749  nnaordex  6760  ectocld  6834  qsel  6845  mapsn  6924  f1oeng  6995  mapen  7098  nneneq  7110  findcard2  7145  findcard2s  7146  ac6sfi  7154  fiintim  7190  sbthlem1  7226  pr2ne  7488  ltbtwnnqq  7729  prnmaddl  7804  genpcdl  7833  genpcuu  7834  ltaddpr  7911  lteupri  7931  recexprlemss1l  7949  recexprlemss1u  7950  cauappcvgprlemdisj  7965  lttrsr  8076  recexgt0sr  8087  mulgt0sr  8092  axprecex  8194  rereceu  8203  addlsub  8642  recexap  8926  0mnnnnn0  9527  prime  9676  zeo  9682  fnn0ind  9693  zindd  9695  btwnz  9696  lbzbi  9947  addmodlteq  10759  facwordi  11101  seq3coll  11210  ccatalpha  11297  pfxccatin12lem2a  11415  qdenre  11883  climcau  12028  serf0  12033  zsumdc  12066  fsum2dlemstep  12116  fsum2d  12117  fsumabs  12147  fsumiun  12159  zproddc  12261  fprod2dlemstep  12304  fprod2d  12305  odd2np1  12555  ndvdssub  12612  bitsinv1lem  12643  dfgcd2  12706  nprm  12816  rpexp  12846  pc2dvds  13024  pcfac  13044  4sqlem12  13096  4sqlem17  13101  divsfval  13533  mulgaddcom  13855  mulginvcom  13856  ringinvnz1ne0  14185  lmss  15103  lmtopcnp  15107  txcn  15132  txlm  15136  xmettri2  15218  blin2  15289  metcnp3  15368  limcresi  15523  dvmptfsum  15582  logbgcd1irr  15824  lgsdir2lem2  15894  lgsne0  15903  2lgsoddprm  15978  2sqlem6  15985  2sqlem10  15990  uhgr0vb  16071  wlk1walkdom  16346  wlkv0  16356  wlklenvclwlk  16360  bj-stim  16510  bj-stan  16511  bj-stand  16512  bj-stal  16513  bj-sbimedh  16535  bj-vtoclgft  16539  elabgft1  16542  elabgf2  16544