Theorem e333

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

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

Proof

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