Theorem mpii 44

Description: A doubly nested modus ponens inference. (Contributed by NM, 31-Dec-1993.) (Proof shortened by Wolf Lammen, 31-Jul-2012.)

Hypotheses

Ref	Expression
mpii.1	|- ch
mpii.2	|- ( ph -> ( ps -> ( ch -> th ) ) )

Assertion

Ref	Expression
mpii	|- ( ph -> ( ps -> th ) )

Proof of Theorem mpii

Step	Hyp	Ref	Expression
1		mpii.1	. . 3 |- ch
2	1	a1i 9	. 2 |- ( ps -> ch )
3		mpii.2	. 2 |- ( ph -> ( ps -> ( ch -> th ) ) )
4	2, 3	mpdi 43	1 |- ( ph -> ( ps -> th ) )

Syntax hints:   -> wi 4

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

This theorem is referenced by:  equveli  1773  intmin  3894  dfiin2g  3949  exmidsssnc  4236  ssorduni  4523  opnneiid  14400