Theorem gen31

Description: Virtual deduction generalizing rule for one quantifying variable and three virtual hypothesis. gen31 is ggen31 with virtual deductions. (Contributed by Alan Sare, 22-Jun-2012) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypothesis	gen31.1	|- (. ph ,. ps ,. ch ->. th ).
Assertion	gen31	|- (. ph ,. ps ,. ch ->. A. x th ).

Proof

Step	Hyp	Ref	Expression
1		gen31.1	|- (. ph ,. ps ,. ch ->. th ).
2	1	dfvd3i	|- ( ph -> ( ps -> ( ch -> th ) ) )
3	2	ggen31	|- ( ph -> ( ps -> ( ch -> A. x th ) ) )
4	3	dfvd3ir	|- (. ph ,. ps ,. ch ->. A. x th ).