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  125  pm3.2i  270  sstri  3156  0disj  3986  disjx0  3988  ontr2exmid  4509  0elsucexmid  4549  relres  4919  cnvdif  5017  funopab4  5235  fun0  5256  fvsn  5691  reltpos  6229  tpostpos  6243  tpos0  6253  oawordriexmid  6449  swoer  6541  xpider  6584  erinxp  6587  domfiexmid  6856  diffitest  6865  pw1dom2  7204  ltrel  7981  lerel  7983  frecfzennn  10382  sum0  11351  qnnen  12386