Theorem e222

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

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

Proof

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