Theorem ee01 16582

Description: e01 16581 without virtual deduction symbols.

Hypotheses

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

Assertion

Ref	Expression
ee01	|- (ps -> th)

Proof of Theorem ee01

Step	Hyp	Ref	Expression
1		ee01.1	. . 3 |- ph
2	1	a1i 8	. 2 |- (ps -> ph)
3		ee01.2	. 2 |- (ps -> ch)
4		ee01.3	. 2 |- (ph -> (ch -> th))
5	2, 3, 4	ee11 1268	1 |- (ps -> th)

Syntax hints:   -> wi 3

This theorem is referenced by:  trsspwALT2 16641  sspwtrALT 16644  snelpwr 16655  sstrALT2 16659

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

Copyright terms: Public domain