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  2726  2ordpr  4295  regexmid  4306  ordsoexmid  4333  reg3exmid  4350  intasym  4759  relcoi1  4899  funres11  5022  cnvresid  5024  mpt2fvex  5880  df1st2  5891  df2nd2  5892  dftpos4  5932  tposf12  5938  frecabcl  6068  xpcomco  6391  ominf  6452  djuin  6556  rec1nq  6699  halfnqq  6714  caucvgsrlemasr  7080  axresscn  7142  0re  7233  gtso  7309  cnegexlem2  7403  uzn0  8767  indstr  8814  dfioo2  9125  hashinfuni  9853  hashp1i  9886  cnrecnv  9998  rexanuz  10075  climdm  10335  lcmgcdlem  10666  3prm  10717  sqpweven  10760  2sqpwodd  10761  qnumval  10770  qdenval  10771  xpnnen  10814