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  1835  exdistrfor  1848  sbcof2  1858  ax11a2  1869  ax11v  1875  sb4  1880  hbsb4t  2066  exmoeudc  2143  euimmo  2147  mopick  2158  r19.37  2686  spcimgft  2883  spcimegft  2885  rr19.28v  2947  mob2  2987  euind  2994  reuind  3012  sbeqalb  3089  triun  4205  csbexga  4222  copsexg  4342  trssord  4483  trsuc  4525  trsucss  4526  abnexg  4549  ralxfrd  4565  rexxfrd  4566  ralxfrALT  4570  sucprcreg  4653  nlimsucg  4670  tfis  4687  relssres  5057  issref  5126  dmsnopg  5215  dfco2a  5244  imadif  5417  fvelima  5706  mptfvex  5741  fvmptdf  5743  fvmptf  5748  funfvima2  5897  funfvima3  5898  foco2  5904  isores3  5966  oprabid  6060  ovmpt4g  6154  ovmpos  6155  ov2gf  6156  ovmpodf  6163  suppssov1  6241  fo2ndf  6401  suppssfvg  6441  rntpos  6466  tposf2  6477  nnmordi  6727  nnmord  6728  nnaordex  6739  ectocld  6813  qsel  6824  mapsn  6902  f1oeng  6973  mapen  7075  nneneq  7086  findcard2  7121  findcard2s  7122  ac6sfi  7130  fiintim  7166  sbthlem1  7199  pr2ne  7440  ltbtwnnqq  7678  prnmaddl  7753  genpcdl  7782  genpcuu  7783  ltaddpr  7860  lteupri  7880  recexprlemss1l  7898  recexprlemss1u  7899  cauappcvgprlemdisj  7914  lttrsr  8025  recexgt0sr  8036  mulgt0sr  8041  axprecex  8143  rereceu  8152  addlsub  8592  recexap  8876  0mnnnnn0  9477  prime  9622  zeo  9628  fnn0ind  9639  zindd  9641  btwnz  9642  lbzbi  9893  addmodlteq  10704  facwordi  11046  seq3coll  11150  ccatalpha  11237  pfxccatin12lem2a  11355  qdenre  11823  climcau  11968  serf0  11973  zsumdc  12006  fsum2dlemstep  12056  fsum2d  12057  fsumabs  12087  fsumiun  12099  zproddc  12201  fprod2dlemstep  12244  fprod2d  12245  odd2np1  12495  ndvdssub  12552  bitsinv1lem  12583  dfgcd2  12646  nprm  12756  rpexp  12786  pc2dvds  12964  pcfac  12984  4sqlem12  13036  4sqlem17  13041  divsfval  13472  mulgaddcom  13794  mulginvcom  13795  ringinvnz1ne0  14124  lmss  15037  lmtopcnp  15041  txcn  15066  txlm  15070  xmettri2  15152  blin2  15223  metcnp3  15302  limcresi  15457  dvmptfsum  15516  logbgcd1irr  15758  lgsdir2lem2  15828  lgsne0  15837  2lgsoddprm  15912  2sqlem6  15919  2sqlem10  15924  uhgr0vb  16005  wlk1walkdom  16280  wlkv0  16290  wlklenvclwlk  16294  bj-stim  16444  bj-stan  16445  bj-stand  16446  bj-stal  16447  bj-sbimedh  16469  bj-vtoclgft  16473  elabgft1  16476  elabgf2  16478