Theorem gen21nv

Description: Virtual deduction form of alrimdh . (Contributed by Alan Sare, 31-Dec-2011) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypotheses	gen21nv.1	|- ( ph -> A. x ph )
	gen21nv.2	|- ( ps -> A. x ps )
	gen21nv.3	|- (. ph ,. ps ->. ch ).
Assertion	gen21nv	|- (. ph ,. ps ->. A. x ch ).

Proof

Step	Hyp	Ref	Expression
1		gen21nv.1	|- ( ph -> A. x ph )
2		gen21nv.2	|- ( ps -> A. x ps )
3		gen21nv.3	|- (. ph ,. ps ->. ch ).
4	3	dfvd2i	|- ( ph -> ( ps -> ch ) )
5	1 2 4	alrimdh	|- ( ph -> ( ps -> A. x ch ) )
6	5	dfvd2ir	|- (. ph ,. ps ->. A. x ch ).