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 ⊢ (𝜒 → (𝜑 → 𝜃))

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used 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  658  pm2.36  816  pm4.72  839  pm2.18dc  867  con1dc  868  jadc  875  pm2.521dcALT  882  con1biimdc  885  condandc  893  pm5.18dc  895  pm2.68dc  906  syl3an2  1312  syl2an23an  1340  xor3dc  1436  alrimdh  1532  spsd  1591  a5i  1596  19.21h  1610  hbnt  1705  hbae  1770  sbiedh  1840  exdistrfor  1853  sbcof2  1863  ax11a2  1874  ax11v  1880  sb4  1885  hbsb4t  2073  exmoeudc  2150  euimmo  2154  mopick  2165  r19.37  2703  spcimgft  2901  spcimegft  2903  rr19.28v  2966  mob2  3006  euind  3013  reuind  3031  sbeqalb  3108  triun  4244  csbexga  4263  copsexg  4386  trssord  4527  trsuc  4569  trsucss  4570  abnexg  4594  ralxfrd  4610  rexxfrd  4611  ralxfrALT  4615  sucprcreg  4698  nlimsucg  4715  tfis  4732  relssres  5103  issref  5173  dmsnopg  5262  dfco2a  5291  imadif  5464  fvelima  5757  mptfvex  5794  fvmptdf  5796  fvmptf  5801  funfvima2  5954  funfvima3  5955  foco2  5962  isores3  6024  oprabid  6120  ovmpt4g  6214  ovmpos  6215  ov2gf  6216  ovmpodf  6223  suppssov1  6302  fo2ndf  6467  suppssfvg  6507  rntpos  6533  tposf2  6544  nnmordi  6794  nnmord  6795  nnaordex  6806  ectocld  6880  qsel  6891  mapsn  6978  f1oeng  7049  mapen  7152  nneneq  7164  findcard2  7199  findcard2s  7200  ac6sfi  7208  fiintim  7244  sbthlem1  7281  pr2ne  7545  ltbtwnnqq  7789  prnmaddl  7864  genpcdl  7893  genpcuu  7894  ltaddpr  7971  lteupri  7991  recexprlemss1l  8009  recexprlemss1u  8010  cauappcvgprlemdisj  8025  lttrsr  8136  recexgt0sr  8147  mulgt0sr  8152  axprecex  8254  rereceu  8263  addlsub  8704  recexap  8990  0mnnnnn0  9607  prime  9756  zeo  9762  fnn0ind  9773  zindd  9775  btwnz  9776  lbzbi  10032  addmodlteq  10856  facwordi  11200  seq3coll  11316  ccatalpha  11403  pfxccatin12lem2a  11521  qdenre  11991  climcau  12138  serf0  12143  zsumdc  12176  fsum2dlemstep  12226  fsum2d  12227  fsumabs  12257  fsumiun  12269  zproddc  12371  fprod2dlemstep  12414  fprod2d  12415  odd2np1  12665  ndvdssub  12722  bitsinv1lem  12753  dfgcd2  12816  nprm  12926  rpexp  12957  pc2dvds  13138  pcfac  13158  4sqlem12  13210  4sqlem17  13215  prmlem0  13249  divsfval  13708  mulgaddcom  14008  mulginvcom  14009  cntz2ss  14168  gsumsnfdcmn  14257  ringinvnz1ne0  14461  lmss  15505  lmtopcnp  15509  txcn  15534  txlm  15538  xmettri2  15620  blin2  15691  metcnp3  15770  limcresi  15925  dvmptfsum  15984  sineq0re  16109  logbgcd1irr  16236  lgsdir2lem2  16386  lgsne0  16395  2lgsoddprm  16470  2sqlem6  16477  2sqlem10  16482  uhgr0vb  16563  wlk1walkdom  16838  wlkv0  16848  wlklenvclwlk  16852  bj-stim  17012  bj-stan  17013  bj-stand  17014  bj-stal  17015  bj-sbimedh  17037  bj-vtoclgft  17041  elabgft1  17044  elabgf2  17046