Theorem el2122old

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

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

Proof

Step	Hyp	Ref	Expression
1		el2122old.1	|- (. (. ph ,. ps ). ->. ch ).
2		el2122old.2	|- (. ps ->. th ).
3		el2122old.3	|- (. ps ->. ta ).
4		el2122old.4	|- ( ( ch /\ th /\ ta ) -> et )
5	1	dfvd2ani	|- ( ( ph /\ ps ) -> ch )
6	2	in1	|- ( ps -> th )
7	3	in1	|- ( ps -> ta )
8	5 6 7 4	eel2122old	|- ( ( ph /\ ps ) -> et )
9	8	dfvd2anir	|- (. (. ph ,. ps ). ->. et ).