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  806  pm4.72  829  pm2.18dc  857  con1dc  858  jadc  865  pm2.521dcALT  872  con1biimdc  875  condandc  883  pm5.18dc  885  pm2.68dc  896  syl3an2  1284  syl2an23an  1312  xor3dc  1407  alrimdh  1503  spsd  1562  a5i  1567  19.21h  1581  hbnt  1677  hbae  1742  sbiedh  1811  exdistrfor  1824  sbcof2  1834  ax11a2  1845  ax11v  1851  sb4  1856  hbsb4t  2042  exmoeudc  2118  euimmo  2122  mopick  2133  r19.37  2659  spcimgft  2851  spcimegft  2853  rr19.28v  2915  mob2  2955  euind  2962  reuind  2980  sbeqalb  3057  triun  4160  csbexga  4177  copsexg  4293  trssord  4432  trsuc  4474  trsucss  4475  abnexg  4498  ralxfrd  4514  rexxfrd  4515  ralxfrALT  4519  sucprcreg  4602  nlimsucg  4619  tfis  4636  relssres  5003  issref  5071  dmsnopg  5160  dfco2a  5189  imadif  5360  fvelima  5640  mptfvex  5675  fvmptdf  5677  fvmptf  5682  funfvima2  5827  funfvima3  5828  foco2  5832  isores3  5894  oprabid  5986  ovmpt4g  6078  ovmpos  6079  ov2gf  6080  ovmpodf  6087  suppssfv  6164  suppssov1  6165  fo2ndf  6323  rntpos  6353  tposf2  6364  nnmordi  6612  nnmord  6613  nnaordex  6624  ectocld  6698  qsel  6709  mapsn  6787  f1oeng  6858  mapen  6955  nneneq  6966  findcard2  6998  findcard2s  6999  ac6sfi  7007  fiintim  7040  sbthlem1  7071  pr2ne  7312  ltbtwnnqq  7541  prnmaddl  7616  genpcdl  7645  genpcuu  7646  ltaddpr  7723  lteupri  7743  recexprlemss1l  7761  recexprlemss1u  7762  cauappcvgprlemdisj  7777  lttrsr  7888  recexgt0sr  7899  mulgt0sr  7904  axprecex  8006  rereceu  8015  addlsub  8455  recexap  8739  0mnnnnn0  9340  prime  9485  zeo  9491  fnn0ind  9502  zindd  9504  btwnz  9505  lbzbi  9750  addmodlteq  10556  facwordi  10898  seq3coll  11000  qdenre  11563  climcau  11708  serf0  11713  zsumdc  11745  fsum2dlemstep  11795  fsum2d  11796  fsumabs  11826  fsumiun  11838  zproddc  11940  fprod2dlemstep  11983  fprod2d  11984  odd2np1  12234  ndvdssub  12291  bitsinv1lem  12322  dfgcd2  12385  nprm  12495  rpexp  12525  pc2dvds  12703  pcfac  12723  4sqlem12  12775  4sqlem17  12780  divsfval  13210  mulgaddcom  13532  mulginvcom  13533  ringinvnz1ne0  13861  lmss  14768  lmtopcnp  14772  txcn  14797  txlm  14801  xmettri2  14883  blin2  14954  metcnp3  15033  limcresi  15188  dvmptfsum  15247  logbgcd1irr  15489  lgsdir2lem2  15556  lgsne0  15565  2lgsoddprm  15640  2sqlem6  15647  2sqlem10  15652  uhgr0vb  15730  bj-stim  15796  bj-stan  15797  bj-stand  15798  bj-stal  15799  bj-sbimedh  15821  bj-vtoclgft  15825  elabgft1  15828  elabgf2  15830