Theorem mp2b 8

Description: A double modus ponens inference. (Contributed by Mario Carneiro, 24-Jan-2013.)

Hypotheses

Ref	Expression
mp2b.1	⊢ 𝜑
mp2b.2	⊢ (𝜑 → 𝜓)
mp2b.3	⊢ (𝜓 → 𝜒)

Assertion

Ref	Expression
mp2b	⊢ 𝜒

Proof of Theorem mp2b

Step	Hyp	Ref	Expression
1		mp2b.1	. . 3 ⊢ 𝜑
2		mp2b.2	. . 3 ⊢ (𝜑 → 𝜓)
3	1, 2	ax-mp 5	. 2 ⊢ 𝜓
4		mp2b.3	. 2 ⊢ (𝜓 → 𝜒)
5	3, 4	ax-mp 5	1 ⊢ 𝜒

Syntax hints:   → wi 4

This theorem was proved from axioms:  ax-mp 5

This theorem is referenced by:  eqvinc  2929  2ordpr  4622  regexmid  4633  ordsoexmid  4660  reg3exmid  4678  intasym  5121  relcoi1  5268  funres11  5402  cnvresid  5404  mpofvex  6370  df1st2  6384  df2nd2  6385  dftpos4  6429  tposf12  6435  frecabcl  6565  xp01disjl  6602  xpcomco  7010  1ndom2  7051  ominf  7085  sbthlem2  7157  djuunr  7265  eldju  7267  ctssdccl  7310  ctssdclemr  7311  omct  7316  ctssexmid  7349  rec1nq  7615  halfnqq  7630  caucvgsrlemasr  8010  axresscn  8080  0re  8179  gtso  8258  cnegexlem2  8355  uzn0  9772  indstr  9827  dfioo2  10209  fnn0nninf  10701  hashinfuni  11040  hashp1i  11075  cnrecnv  11472  rexanuz  11550  xrmaxiflemcom  11811  climdm  11857  sumsnf  11972  tanvalap  12271  egt2lt3  12343  lcmgcdlem  12651  3prm  12702  sqpweven  12749  2sqpwodd  12750  qnumval  12759  qdenval  12760  modxai  12991  xpnnen  13017  ennnfonelemhdmp1  13032  ennnfonelemss  13033  ennnfonelemnn0  13045  qnnen  13054  ctiunctal  13064  unct  13065  structcnvcnv  13100  setsslid  13135  prdsvallem  13357  prdsval  13358  xpsfrn  13435  xpsff1o2  13436  ringn0  14076  rmodislmodlem  14367  cnfldstr  14575  cnfldadd  14579  cnfldmul  14581  cnfldsub  14592  cnsubmlem  14595  cnsubglem  14596  zring0  14617  tgrest  14896  lmbr2  14941  cnptoprest  14966  lmff  14976  tx1cn  14996  tx2cn  14997  cnblcld  15262  cnfldms  15263  cnfldtopn  15266  tgioo  15281  reeff1o  15500  pilem1  15506  efhalfpi  15526  coseq0negpitopi  15563  pw1ninf  16611  012of  16613  pw1nct  16625  nnnninfen  16644  iswomninnlem  16674