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  3236  0disj  4085  disjx0  4087  ontr2exmid  4623  0elsucexmid  4663  relres  5041  cnvdif  5143  funopab4  5363  fun0  5388  fvsn  5849  reltpos  6416  tpostpos  6430  tpos0  6440  oawordriexmid  6638  swoer  6730  xpider  6775  erinxp  6778  domfiexmid  7067  diffitest  7076  pw1dom2  7445  ltrel  8241  lerel  8243  frecfzennn  10689  sum0  11951  qnnen  13054  hovercncf  15373  lgsquadlem1  15809  lgsquadlem2  15810  usgrexmpldifpr  16103