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  3234  0disj  4083  disjx0  4085  ontr2exmid  4621  0elsucexmid  4661  relres  5039  cnvdif  5141  funopab4  5361  fun0  5385  fvsn  5844  reltpos  6411  tpostpos  6425  tpos0  6435  oawordriexmid  6633  swoer  6725  xpider  6770  erinxp  6773  domfiexmid  7062  diffitest  7071  pw1dom2  7438  ltrel  8234  lerel  8236  frecfzennn  10681  sum0  11942  qnnen  13045  hovercncf  15363  lgsquadlem1  15799  lgsquadlem2  15800  usgrexmpldifpr  16093