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  2689  2ordpr  4276  regexmid  4287  ordsoexmid  4313  reg3exmid  4331  intasym  4736  relcoi1  4876  funres11  4998  cnvresid  5000  mpt2fvex  5856  df1st2  5867  df2nd2  5868  dftpos4  5908  tposf12  5914  xpcomco  6330  rec1nq  6550  halfnqq  6565  caucvgsrlemasr  6931  axresscn  6993  0re  7084  gtso  7155  cnegexlem2  7249  uzn0  8583  indstr  8631  dfioo2  8943  cnrecnv  9731  rexanuz  9808  climdm  10039