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 7	. 2 ⊢ 𝜓
4		mp2b.3	. 2 ⊢ (𝜓 → 𝜒)
5	3, 4	ax-mp 7	1 ⊢ 𝜒

Syntax hints:   → wi 4

This theorem was proved from axioms:  ax-mp 7

This theorem is referenced by:  eqvinc  2740  2ordpr  4340  regexmid  4351  ordsoexmid  4378  reg3exmid  4395  intasym  4816  relcoi1  4962  funres11  5086  cnvresid  5088  mpt2fvex  5973  df1st2  5984  df2nd2  5985  dftpos4  6028  tposf12  6034  frecabcl  6164  xpcomco  6542  ominf  6612  sbthlem2  6667  djuin  6756  djuunr  6758  eldju  6759  rec1nq  6954  halfnqq  6969  caucvgsrlemasr  7335  axresscn  7397  0re  7488  gtso  7564  cnegexlem2  7658  uzn0  9034  indstr  9081  dfioo2  9392  fnn0nninf  9843  hashinfuni  10185  hashp1i  10218  cnrecnv  10344  rexanuz  10421  climdm  10683  sumsnf  10803  tanvalap  10999  egt2lt3  11067  lcmgcdlem  11337  3prm  11388  sqpweven  11431  2sqpwodd  11432  qnumval  11441  qdenval  11442  xpnnen  11485  structcnvcnv  11510  setsslid  11544