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  3162  0disj  3995  disjx0  3997  ontr2exmid  4518  0elsucexmid  4558  relres  4928  cnvdif  5027  funopab4  5245  fun0  5266  fvsn  5703  reltpos  6241  tpostpos  6255  tpos0  6265  oawordriexmid  6461  swoer  6553  xpider  6596  erinxp  6599  domfiexmid  6868  diffitest  6877  pw1dom2  7216  ltrel  7993  lerel  7995  frecfzennn  10394  sum0  11362  qnnen  12397