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  4242  csbexga  4261  copsexg  4384  trssord  4525  trsuc  4567  trsucss  4568  abnexg  4592  ralxfrd  4608  rexxfrd  4609  ralxfrALT  4613  sucprcreg  4696  nlimsucg  4713  tfis  4730  relssres  5101  issref  5170  dmsnopg  5259  dfco2a  5288  imadif  5461  fvelima  5754  mptfvex  5791  fvmptdf  5793  fvmptf  5798  funfvima2  5951  funfvima3  5952  foco2  5959  isores3  6021  oprabid  6117  ovmpt4g  6211  ovmpos  6212  ov2gf  6213  ovmpodf  6220  suppssov1  6299  fo2ndf  6463  suppssfvg  6503  rntpos  6528  tposf2  6539  nnmordi  6789  nnmord  6790  nnaordex  6801  ectocld  6875  qsel  6886  mapsn  6972  f1oeng  7043  mapen  7146  nneneq  7158  findcard2  7193  findcard2s  7194  ac6sfi  7202  fiintim  7238  sbthlem1  7274  pr2ne  7539  ltbtwnnqq  7783  prnmaddl  7858  genpcdl  7887  genpcuu  7888  ltaddpr  7965  lteupri  7985  recexprlemss1l  8003  recexprlemss1u  8004  cauappcvgprlemdisj  8019  lttrsr  8130  recexgt0sr  8141  mulgt0sr  8146  axprecex  8248  rereceu  8257  addlsub  8698  recexap  8984  0mnnnnn0  9600  prime  9750  zeo  9756  fnn0ind  9767  zindd  9769  btwnz  9770  lbzbi  10026  addmodlteq  10849  facwordi  11193  seq3coll  11309  ccatalpha  11396  pfxccatin12lem2a  11514  qdenre  11984  climcau  12131  serf0  12136  zsumdc  12169  fsum2dlemstep  12219  fsum2d  12220  fsumabs  12250  fsumiun  12262  zproddc  12364  fprod2dlemstep  12407  fprod2d  12408  odd2np1  12658  ndvdssub  12715  bitsinv1lem  12746  dfgcd2  12809  nprm  12919  rpexp  12950  pc2dvds  13131  pcfac  13151  4sqlem12  13203  4sqlem17  13208  prmlem0  13242  divsfval  13700  mulgaddcom  14000  mulginvcom  14001  ringinvnz1ne0  14405  lmss  15399  lmtopcnp  15403  txcn  15428  txlm  15432  xmettri2  15514  blin2  15585  metcnp3  15664  limcresi  15819  dvmptfsum  15878  logbgcd1irr  16125  lgsdir2lem2  16270  lgsne0  16279  2lgsoddprm  16354  2sqlem6  16361  2sqlem10  16366  uhgr0vb  16447  wlk1walkdom  16722  wlkv0  16732  wlklenvclwlk  16736  bj-stim  16896  bj-stan  16897  bj-stand  16898  bj-stal  16899  bj-sbimedh  16921  bj-vtoclgft  16925  elabgft1  16928  elabgf2  16930