Theorem e222 38861

Description: A virtual deduction elimination rule. (Contributed by Alan Sare, 12-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

Hypotheses

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

Assertion

Ref	Expression
e222	|- (. ph ,. ps ->. et ).

Proof of Theorem e222

Step	Hyp	Ref	Expression
1		e222.3	. . . . . . 7 |- (. ph ,. ps ->. ta ).
2	1	dfvd2i 38801	. . . . . 6 |- ( ph -> ( ps -> ta ) )
3	2	imp 445	. . . . 5 |- ( ( ph /\ ps ) -> ta )
4		e222.1	. . . . . . . . 9 |- (. ph ,. ps ->. ch ).
5	4	dfvd2i 38801	. . . . . . . 8 |- ( ph -> ( ps -> ch ) )
6	5	imp 445	. . . . . . 7 |- ( ( ph /\ ps ) -> ch )
7		e222.2	. . . . . . . . 9 |- (. ph ,. ps ->. th ).
8	7	dfvd2i 38801	. . . . . . . 8 |- ( ph -> ( ps -> th ) )
9	8	imp 445	. . . . . . 7 |- ( ( ph /\ ps ) -> th )
10		e222.4	. . . . . . 7 |- ( ch -> ( th -> ( ta -> et ) ) )
11	6, 9, 10	syl2im 40	. . . . . 6 |- ( ( ph /\ ps ) -> ( ( ph /\ ps ) -> ( ta -> et ) ) )
12	11	pm2.43i 52	. . . . 5 |- ( ( ph /\ ps ) -> ( ta -> et ) )
13	3, 12	syl5com 31	. . . 4 |- ( ( ph /\ ps ) -> ( ( ph /\ ps ) -> et ) )
14	13	pm2.43i 52	. . 3 |- ( ( ph /\ ps ) -> et )
15	14	ex 450	. 2 |- ( ph -> ( ps -> et ) )
16	15	dfvd2ir 38802	1 |- (. ph ,. ps ->. et ).

Syntax hints:   -> wi 4   /\ wa 384   (.wvd2 38793

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  df-vd2 38794

This theorem is referenced by:  e220  38862  e202  38864  e022  38866  e002  38868  e020  38870  e200  38872  e221  38874  e212  38876  e122  38878  e112  38879  e121  38881  e211  38882  e22  38896  suctrALT2VD  39071  en3lplem2VD  39079  19.21a3con13vVD  39087  tratrbVD  39097