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  7538  ltbtwnnqq  7782  prnmaddl  7857  genpcdl  7886  genpcuu  7887  ltaddpr  7964  lteupri  7984  recexprlemss1l  8002  recexprlemss1u  8003  cauappcvgprlemdisj  8018  lttrsr  8129  recexgt0sr  8140  mulgt0sr  8145  axprecex  8247  rereceu  8256  addlsub  8696  recexap  8982  0mnnnnn0  9597  prime  9747  zeo  9753  fnn0ind  9764  zindd  9766  btwnz  9767  lbzbi  10018  addmodlteq  10837  facwordi  11180  seq3coll  11296  ccatalpha  11383  pfxccatin12lem2a  11501  qdenre  11970  climcau  12115  serf0  12120  zsumdc  12153  fsum2dlemstep  12203  fsum2d  12204  fsumabs  12234  fsumiun  12246  zproddc  12348  fprod2dlemstep  12391  fprod2d  12392  odd2np1  12642  ndvdssub  12699  bitsinv1lem  12730  dfgcd2  12793  nprm  12903  rpexp  12933  pc2dvds  13111  pcfac  13131  4sqlem12  13183  4sqlem17  13188  divsfval  13651  mulgaddcom  13951  mulginvcom  13952  ringinvnz1ne0  14356  lmss  15349  lmtopcnp  15353  txcn  15378  txlm  15382  xmettri2  15464  blin2  15535  metcnp3  15614  limcresi  15769  dvmptfsum  15828  logbgcd1irr  16075  lgsdir2lem2  16160  lgsne0  16169  2lgsoddprm  16244  2sqlem6  16251  2sqlem10  16256  uhgr0vb  16337  wlk1walkdom  16612  wlkv0  16622  wlklenvclwlk  16626  bj-stim  16786  bj-stan  16787  bj-stand  16788  bj-stal  16789  bj-sbimedh  16811  bj-vtoclgft  16815  elabgft1  16818  elabgf2  16820