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  3233  0disj  4080  disjx0  4082  ontr2exmid  4618  0elsucexmid  4658  relres  5036  cnvdif  5138  funopab4  5358  fun0  5382  fvsn  5841  reltpos  6407  tpostpos  6421  tpos0  6431  oawordriexmid  6629  swoer  6721  xpider  6766  erinxp  6769  domfiexmid  7053  diffitest  7062  pw1dom2  7428  ltrel  8224  lerel  8226  frecfzennn  10665  sum0  11920  qnnen  13023  hovercncf  15341  lgsquadlem1  15777  lgsquadlem2  15778  usgrexmpldifpr  16068