Theorem mp2 16

Description: A double modus ponens inference. (Contributed by NM, 5-Apr-1994.) (Proof shortened by Wolf Lammen, 23-Jul-2013.)

Hypotheses

Ref	Expression
mp2.1	⊢ 𝜑
mp2.2	⊢ 𝜓
mp2.3	⊢ (𝜑 → (𝜓 → 𝜒))

Assertion

Ref	Expression
mp2	⊢ 𝜒

Proof of Theorem mp2

Step	Hyp	Ref	Expression
1		mp2.1	. 2 ⊢ 𝜑
2		mp2.2	. . 3 ⊢ 𝜓
3		mp2.3	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
4	2, 3	mpi 15	. 2 ⊢ (𝜑 → 𝜒)
5	1, 4	ax-mp 5	1 ⊢ 𝜒

Syntax hints:   → wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is referenced by:  impbii  126  pm3.2i  272  sstri  3164  0disj  4000  disjx0  4002  ontr2exmid  4524  0elsucexmid  4564  relres  4935  cnvdif  5035  funopab4  5253  fun0  5274  fvsn  5711  reltpos  6250  tpostpos  6264  tpos0  6274  oawordriexmid  6470  swoer  6562  xpider  6605  erinxp  6608  domfiexmid  6877  diffitest  6886  pw1dom2  7225  ltrel  8018  lerel  8020  frecfzennn  10425  sum0  11395  qnnen  12431