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  3233  0disj  4080  disjx0  4082  ontr2exmid  4617  0elsucexmid  4657  relres  5033  cnvdif  5135  funopab4  5355  fun0  5379  fvsn  5838  reltpos  6402  tpostpos  6416  tpos0  6426  oawordriexmid  6624  swoer  6716  xpider  6761  erinxp  6764  domfiexmid  7048  diffitest  7057  pw1dom2  7420  ltrel  8216  lerel  8218  frecfzennn  10656  sum0  11907  qnnen  13010  hovercncf  15328  lgsquadlem1  15764  lgsquadlem2  15765