Theorem e233

Description: A virtual deduction elimination rule. (Contributed by Alan Sare, 29-Feb-2012) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		e233.1	|- (. ph ,. ps ->. ch ).
2		e233.2	|- (. ph ,. ps ,. th ->. ta ).
3		e233.3	|- (. ph ,. ps ,. th ->. et ).
4		e233.4	|- ( ch -> ( ta -> ( et -> ze ) ) )
5	1	dfvd2i	|- ( ph -> ( ps -> ch ) )
6	2	dfvd3i	|- ( ph -> ( ps -> ( th -> ta ) ) )
7	3	dfvd3i	|- ( ph -> ( ps -> ( th -> et ) ) )
8	5 6 7 4	ee233	|- ( ph -> ( ps -> ( th -> ze ) ) )
9	8	dfvd3ir	|- (. ph ,. ps ,. th ->. ze ).