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  3165  0disj  4001  disjx0  4003  ontr2exmid  4525  0elsucexmid  4565  relres  4936  cnvdif  5036  funopab4  5254  fun0  5275  fvsn  5712  reltpos  6251  tpostpos  6265  tpos0  6275  oawordriexmid  6471  swoer  6563  xpider  6606  erinxp  6609  domfiexmid  6878  diffitest  6887  pw1dom2  7226  ltrel  8019  lerel  8021  frecfzennn  10426  sum0  11396  qnnen  12432