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  6532  tposf2  6543  nnmordi  6793  nnmord  6794  nnaordex  6805  ectocld  6879  qsel  6890  mapsn  6977  f1oeng  7048  mapen  7151  nneneq  7163  findcard2  7198  findcard2s  7199  ac6sfi  7207  fiintim  7243  sbthlem1  7280  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  9757  zeo  9763  fnn0ind  9774  zindd  9776  btwnz  9777  lbzbi  10033  addmodlteq  10857  facwordi  11201  seq3coll  11317  ccatalpha  11404  pfxccatin12lem2a  11522  qdenre  11992  climcau  12139  serf0  12144  zsumdc  12177  fsum2dlemstep  12227  fsum2d  12228  fsumabs  12258  fsumiun  12270  zproddc  12372  fprod2dlemstep  12415  fprod2d  12416  odd2np1  12666  ndvdssub  12723  bitsinv1lem  12754  dfgcd2  12817  nprm  12927  rpexp  12958  pc2dvds  13139  pcfac  13159  4sqlem12  13211  4sqlem17  13216  prmlem0  13250  divsfval  13709  mulgaddcom  14009  mulginvcom  14010  cntz2ss  14169  gsumsnfdcmn  14258  ringinvnz1ne0  14462  lmss  15484  lmtopcnp  15488  txcn  15513  txlm  15517  xmettri2  15599  blin2  15670  metcnp3  15749  limcresi  15904  dvmptfsum  15963  sineq0re  16088  logbgcd1irr  16215  lgsdir2lem2  16365  lgsne0  16374  2lgsoddprm  16449  2sqlem6  16456  2sqlem10  16461  uhgr0vb  16542  wlk1walkdom  16817  wlkv0  16827  wlklenvclwlk  16831  bj-stim  16991  bj-stan  16992  bj-stand  16993  bj-stal  16994  bj-sbimedh  17016  bj-vtoclgft  17020  elabgft1  17023  elabgf2  17025