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  2860  2ordpr  4523  regexmid  4534  ordsoexmid  4561  reg3exmid  4579  intasym  5013  relcoi1  5160  funres11  5288  cnvresid  5290  mpofvex  6203  df1st2  6219  df2nd2  6220  dftpos4  6263  tposf12  6269  frecabcl  6399  xp01disjl  6434  xpcomco  6825  ominf  6895  sbthlem2  6956  djuunr  7064  eldju  7066  ctssdccl  7109  ctssdclemr  7110  omct  7115  ctssexmid  7147  rec1nq  7393  halfnqq  7408  caucvgsrlemasr  7788  axresscn  7858  0re  7956  gtso  8035  cnegexlem2  8132  uzn0  9542  indstr  9592  dfioo2  9973  fnn0nninf  10436  hashinfuni  10756  hashp1i  10789  cnrecnv  10918  rexanuz  10996  xrmaxiflemcom  11256  climdm  11302  sumsnf  11416  tanvalap  11715  egt2lt3  11786  lcmgcdlem  12076  3prm  12127  sqpweven  12174  2sqpwodd  12175  qnumval  12184  qdenval  12185  xpnnen  12394  ennnfonelemhdmp1  12409  ennnfonelemss  12410  ennnfonelemnn0  12422  qnnen  12431  ctiunctal  12441  unct  12442  structcnvcnv  12477  setsslid  12512  xpsfrn  12768  xpsff1o2  12769  ringn0  13235  cnfldsub  13439  cnsubmlem  13442  cnsubglem  13443  zring0  13460  tgrest  13639  lmbr2  13684  cnptoprest  13709  lmff  13719  tx1cn  13739  tx2cn  13740  cnblcld  14005  tgioo  14016  reeff1o  14164  pilem1  14170  efhalfpi  14190  coseq0negpitopi  14227  012of  14715  pw1nct  14722  iswomninnlem  14767