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  3257  0disj  4125  disjx0  4127  ontr2exmid  4670  0elsucexmid  4710  relres  5089  cnvdif  5192  funopab4  5412  fun0  5437  fvsn  5904  reltpos  6515  tpostpos  6529  tpos0  6539  oawordriexmid  6737  swoer  6829  xpider  6874  erinxp  6877  domfiexmid  7176  diffitest  7185  pw1dom2  7580  ltrel  8381  lerel  8383  frecfzennn  10846  sum0  12138  qnnen  13305  hovercncf  15730  lgsquadlem1  16179  lgsquadlem2  16180  usgrexmpldifpr  16473