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  2897  2ordpr  4576  regexmid  4587  ordsoexmid  4614  reg3exmid  4632  intasym  5072  relcoi1  5219  funres11  5351  cnvresid  5353  mpofvex  6298  df1st2  6312  df2nd2  6313  dftpos4  6356  tposf12  6362  frecabcl  6492  xp01disjl  6527  xpcomco  6928  ominf  7000  sbthlem2  7067  djuunr  7175  eldju  7177  ctssdccl  7220  ctssdclemr  7221  omct  7226  ctssexmid  7259  rec1nq  7515  halfnqq  7530  caucvgsrlemasr  7910  axresscn  7980  0re  8079  gtso  8158  cnegexlem2  8255  uzn0  9671  indstr  9721  dfioo2  10103  fnn0nninf  10590  hashinfuni  10929  hashp1i  10962  cnrecnv  11265  rexanuz  11343  xrmaxiflemcom  11604  climdm  11650  sumsnf  11764  tanvalap  12063  egt2lt3  12135  lcmgcdlem  12443  3prm  12494  sqpweven  12541  2sqpwodd  12542  qnumval  12551  qdenval  12552  modxai  12783  xpnnen  12809  ennnfonelemhdmp1  12824  ennnfonelemss  12825  ennnfonelemnn0  12837  qnnen  12846  ctiunctal  12856  unct  12857  structcnvcnv  12892  setsslid  12927  prdsvallem  13148  prdsval  13149  xpsfrn  13226  xpsff1o2  13227  ringn0  13866  rmodislmodlem  14156  cnfldstr  14364  cnfldadd  14368  cnfldmul  14370  cnfldsub  14381  cnsubmlem  14384  cnsubglem  14385  zring0  14406  tgrest  14685  lmbr2  14730  cnptoprest  14755  lmff  14765  tx1cn  14785  tx2cn  14786  cnblcld  15051  cnfldms  15052  cnfldtopn  15055  tgioo  15070  reeff1o  15289  pilem1  15295  efhalfpi  15315  coseq0negpitopi  15352  012of  16004  pw1nct  16014  nnnninfen  16032  iswomninnlem  16062