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  3249  0disj  4108  disjx0  4110  ontr2exmid  4649  0elsucexmid  4689  relres  5068  cnvdif  5171  funopab4  5391  fun0  5416  fvsn  5881  reltpos  6483  tpostpos  6497  tpos0  6507  oawordriexmid  6705  swoer  6797  xpider  6842  erinxp  6845  domfiexmid  7137  diffitest  7146  pw1dom2  7539  ltrel  8340  lerel  8342  frecfzennn  10795  sum0  12082  qnnen  13203  hovercncf  15560  lgsquadlem1  15999  lgsquadlem2  16000  usgrexmpldifpr  16293