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  2875  2ordpr  4538  regexmid  4549  ordsoexmid  4576  reg3exmid  4594  intasym  5028  relcoi1  5175  funres11  5303  cnvresid  5305  mpofvex  6222  df1st2  6238  df2nd2  6239  dftpos4  6282  tposf12  6288  frecabcl  6418  xp01disjl  6453  xpcomco  6844  ominf  6914  sbthlem2  6975  djuunr  7083  eldju  7085  ctssdccl  7128  ctssdclemr  7129  omct  7134  ctssexmid  7166  rec1nq  7412  halfnqq  7427  caucvgsrlemasr  7807  axresscn  7877  0re  7975  gtso  8054  cnegexlem2  8151  uzn0  9561  indstr  9611  dfioo2  9992  fnn0nninf  10455  hashinfuni  10775  hashp1i  10808  cnrecnv  10937  rexanuz  11015  xrmaxiflemcom  11275  climdm  11321  sumsnf  11435  tanvalap  11734  egt2lt3  11805  lcmgcdlem  12095  3prm  12146  sqpweven  12193  2sqpwodd  12194  qnumval  12203  qdenval  12204  xpnnen  12413  ennnfonelemhdmp1  12428  ennnfonelemss  12429  ennnfonelemnn0  12441  qnnen  12450  ctiunctal  12460  unct  12461  structcnvcnv  12496  setsslid  12531  xpsfrn  12792  xpsff1o2  12793  ringn0  13373  rmodislmodlem  13627  cnfldsub  13839  cnsubmlem  13842  cnsubglem  13843  zring0  13860  tgrest  14066  lmbr2  14111  cnptoprest  14136  lmff  14146  tx1cn  14166  tx2cn  14167  cnblcld  14432  tgioo  14443  reeff1o  14591  pilem1  14597  efhalfpi  14617  coseq0negpitopi  14654  012of  15143  pw1nct  15150  iswomninnlem  15195