Theorem e123

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

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

Proof

Step	Hyp	Ref	Expression
1		e123.1	|- (. ph ->. ps ).
2		e123.2	|- (. ph ,. ch ->. th ).
3		e123.3	|- (. ph ,. ch ,. ta ->. et ).
4		e123.4	|- ( ps -> ( th -> ( et -> ze ) ) )
5	1	vd13	|- (. ph ,. ch ,. ta ->. ps ).
6	2	vd23	|- (. ph ,. ch ,. ta ->. th ).
7	5 6 3 4	e333	|- (. ph ,. ch ,. ta ->. ze ).