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  3246  0disj  4105  disjx0  4107  ontr2exmid  4646  0elsucexmid  4686  relres  5065  cnvdif  5168  funopab4  5388  fun0  5413  fvsn  5878  reltpos  6480  tpostpos  6494  tpos0  6504  oawordriexmid  6702  swoer  6794  xpider  6839  erinxp  6842  domfiexmid  7134  diffitest  7143  pw1dom2  7536  ltrel  8331  lerel  8333  frecfzennn  10784  sum0  12067  qnnen  13171  hovercncf  15498  lgsquadlem1  15937  lgsquadlem2  15938  usgrexmpldifpr  16231