Theorem ee222 38708

Description: e222 38861 without virtual deduction connectives. Special theorem needed for the Virtual Deduction translation tool. (Contributed by Alan Sare, 7-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

Hypotheses

Ref	Expression
ee222.1	|- ( ph -> ( ps -> ch ) )
ee222.2	|- ( ph -> ( ps -> th ) )
ee222.3	|- ( ph -> ( ps -> ta ) )
ee222.4	|- ( ch -> ( th -> ( ta -> et ) ) )

Assertion

Ref	Expression
ee222	|- ( ph -> ( ps -> et ) )

Proof of Theorem ee222

Step	Hyp	Ref	Expression
1		ee222.1	. . . 4 |- ( ph -> ( ps -> ch ) )
2	1	imp 445	. . 3 |- ( ( ph /\ ps ) -> ch )
3		ee222.2	. . . 4 |- ( ph -> ( ps -> th ) )
4	3	imp 445	. . 3 |- ( ( ph /\ ps ) -> th )
5		ee222.3	. . . 4 |- ( ph -> ( ps -> ta ) )
6	5	imp 445	. . 3 |- ( ( ph /\ ps ) -> ta )
7		ee222.4	. . 3 |- ( ch -> ( th -> ( ta -> et ) ) )
8	2, 4, 6, 7	syl3c 66	. 2 |- ( ( ph /\ ps ) -> et )
9	8	ex 450	1 |- ( ph -> ( ps -> et ) )

Syntax hints:   -> wi 4   /\ wa 384

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

This theorem depends on definitions:  df-bi 197  df-an 386

This theorem is referenced by:  ee121  38711  ee122  38712  tratrb  38746  ee220  38863  ee202  38865  ee022  38867  ee002  38869  ee020  38871  ee200  38873  ee221  38875  ee212  38877  ee112  38880  ee211  38883  ee210  38885  ee201  38887  ee120  38889  ee021  38891  ee012  38893  ee102  38895  suctrALT2  39072