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	|- ph
mp2.2	|- ps
mp2.3	|- ( ph -> ( ps -> ch ) )

Assertion

Ref	Expression
mp2	|- ch

Proof of Theorem mp2

Step	Hyp	Ref	Expression
1		mp2.1	. 2 |- ph
2		mp2.2	. . 3 |- ps
3		mp2.3	. . 3 |- ( ph -> ( ps -> ch ) )
4	2, 3	mpi 15	. 2 |- ( ph -> ch )
5	1, 4	ax-mp 7	1 |- ch

Syntax hints:   -> wi 4

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7

This theorem is referenced by:  impbii  124  pm3.2i  266  sstri  3034  0disj  3842  disjx0  3844  ontr2exmid  4341  0elsucexmid  4381  relres  4741  cnvdif  4838  funopab4  5051  fun0  5072  fvsn  5492  reltpos  6015  tpostpos  6029  tpos0  6039  oawordriexmid  6231  swoer  6318  xpiderm  6361  erinxp  6364  domfiexmid  6592  diffitest  6601  ltrel  7546  lerel  7548  frecfzennn  9829  sum0  10776  pw1dom2  11844