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  650  pm2.36  805  pm4.72  828  pm2.18dc  856  con1dc  857  jadc  864  pm2.521dcALT  871  con1biimdc  874  condandc  882  pm5.18dc  884  pm2.68dc  895  annimdc  938  syl3an2  1282  syl2an23an  1309  xor3dc  1397  alrimdh  1489  spsd  1548  a5i  1553  19.21h  1567  hbnt  1663  hbae  1728  sbiedh  1797  exdistrfor  1810  sbcof2  1820  ax11a2  1831  ax11v  1837  sb4  1842  hbsb4t  2024  exmoeudc  2100  euimmo  2104  mopick  2115  r19.37  2641  spcimgft  2827  spcimegft  2829  rr19.28v  2891  mob2  2931  euind  2938  reuind  2956  sbeqalb  3033  triun  4128  csbexga  4145  copsexg  4258  trssord  4394  trsuc  4436  trsucss  4437  abnexg  4460  ralxfrd  4476  rexxfrd  4477  ralxfrALT  4481  sucprcreg  4562  nlimsucg  4579  tfis  4596  relssres  4959  issref  5025  dmsnopg  5114  dfco2a  5143  imadif  5310  fvelima  5582  mptfvex  5616  fvmptdf  5618  fvmptf  5623  funfvima2  5764  funfvima3  5765  foco2  5769  isores3  5831  oprabid  5922  ovmpt4g  6013  ovmpos  6014  ov2gf  6015  ovmpodf  6022  suppssfv  6096  suppssov1  6097  fo2ndf  6245  rntpos  6275  tposf2  6286  nnmordi  6534  nnmord  6535  nnaordex  6546  ectocld  6618  qsel  6629  mapsn  6707  f1oeng  6774  mapen  6863  nneneq  6874  findcard2  6906  findcard2s  6907  ac6sfi  6915  fiintim  6945  sbthlem1  6973  pr2ne  7208  ltbtwnnqq  7431  prnmaddl  7506  genpcdl  7535  genpcuu  7536  ltaddpr  7613  lteupri  7633  recexprlemss1l  7651  recexprlemss1u  7652  cauappcvgprlemdisj  7667  lttrsr  7778  recexgt0sr  7789  mulgt0sr  7794  axprecex  7896  rereceu  7905  addlsub  8344  recexap  8627  0mnnnnn0  9225  prime  9369  zeo  9375  fnn0ind  9386  zindd  9388  btwnz  9389  lbzbi  9633  addmodlteq  10415  facwordi  10737  seq3coll  10839  qdenre  11228  climcau  11372  serf0  11377  zsumdc  11409  fsum2dlemstep  11459  fsum2d  11460  fsumabs  11490  fsumiun  11502  zproddc  11604  fprod2dlemstep  11647  fprod2d  11648  odd2np1  11895  ndvdssub  11952  dfgcd2  12032  nprm  12140  rpexp  12170  pc2dvds  12346  pcfac  12365  mulgaddcom  13051  mulginvcom  13052  ringinvnz1ne0  13361  lmss  14129  lmtopcnp  14133  txcn  14158  txlm  14162  xmettri2  14244  blin2  14315  metcnp3  14394  limcresi  14518  logbgcd1irr  14768  lgsdir2lem2  14813  lgsne0  14822  2sqlem6  14850  2sqlem10  14855  bj-stim  14881  bj-stan  14882  bj-stand  14883  bj-stal  14884  bj-sbimedh  14906  bj-vtoclgft  14910  elabgft1  14913  elabgf2  14915