Theorem mpii 45

Description: A doubly nested modus ponens inference.

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	. 2 |- ch
2		mpii.2	. . 3 |- (ph -> (ps -> (ch -> th)))
3	2	com23 32	. 2 |- (ph -> (ch -> (ps -> th)))
4	1, 3	mpi 44	1 |- (ph -> (ps -> th))

Syntax hints:   -> wi 3

This theorem is referenced by:  mpan2i 699  a12lem1 1376  sbciegf 1960  intmin 2553  frirr 2924  ssorduni 2993  suceloni 3062  tfrlem1 3911  rankr1lem 4673  rankval3 4681  bndrank 4682  opnneiid 7737  lmuni 7951  mdbr3 10224  mdbr4 10225  dmdbr5 10235  homindlem3 10551  idfisf 10760

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

Copyright terms: Public domain