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  2927  2ordpr  4620  regexmid  4631  ordsoexmid  4658  reg3exmid  4676  intasym  5119  relcoi1  5266  funres11  5399  cnvresid  5401  mpofvex  6365  df1st2  6379  df2nd2  6380  dftpos4  6424  tposf12  6430  frecabcl  6560  xp01disjl  6597  xpcomco  7005  1ndom2  7046  ominf  7080  sbthlem2  7151  djuunr  7259  eldju  7261  ctssdccl  7304  ctssdclemr  7305  omct  7310  ctssexmid  7343  rec1nq  7608  halfnqq  7623  caucvgsrlemasr  8003  axresscn  8073  0re  8172  gtso  8251  cnegexlem2  8348  uzn0  9765  indstr  9820  dfioo2  10202  fnn0nninf  10693  hashinfuni  11032  hashp1i  11067  cnrecnv  11464  rexanuz  11542  xrmaxiflemcom  11803  climdm  11849  sumsnf  11963  tanvalap  12262  egt2lt3  12334  lcmgcdlem  12642  3prm  12693  sqpweven  12740  2sqpwodd  12741  qnumval  12750  qdenval  12751  modxai  12982  xpnnen  13008  ennnfonelemhdmp1  13023  ennnfonelemss  13024  ennnfonelemnn0  13036  qnnen  13045  ctiunctal  13055  unct  13056  structcnvcnv  13091  setsslid  13126  prdsvallem  13348  prdsval  13349  xpsfrn  13426  xpsff1o2  13427  ringn0  14066  rmodislmodlem  14357  cnfldstr  14565  cnfldadd  14569  cnfldmul  14571  cnfldsub  14582  cnsubmlem  14585  cnsubglem  14586  zring0  14607  tgrest  14886  lmbr2  14931  cnptoprest  14956  lmff  14966  tx1cn  14986  tx2cn  14987  cnblcld  15252  cnfldms  15253  cnfldtopn  15256  tgioo  15271  reeff1o  15490  pilem1  15496  efhalfpi  15516  coseq0negpitopi  15553  pw1ninf  16540  012of  16542  pw1nct  16554  nnnninfen  16573  iswomninnlem  16603