Theorem gen12 38843

Description: Virtual deduction generalizing rule for two quantifying variables and one virtual hypothesis. gen12 38843 is alrimivv 1856 with virtual deductions. (Contributed by Alan Sare, 2-May-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

Hypothesis

Ref	Expression
gen12.1	|- (. ph ->. ps ).

Assertion

Ref	Expression
gen12	|- (. ph ->. A. x A. y ps ).

Distinct variable groups:   ph, x   ph, y

Allowed substitution hints:   ps( x, y)

Proof of Theorem gen12

Step	Hyp	Ref	Expression
1		gen12.1	. . . 4 |- (. ph ->. ps ).
2	1	in1 38787	. . 3 |- ( ph -> ps )
3	2	alrimivv 1856	. 2 |- ( ph -> A. x A. y ps )
4	3	dfvd1ir 38789	1 |- (. ph ->. A. x A. y ps ).

Syntax hints:   A.wal 1481   (.wvd1 38785

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839

This theorem depends on definitions:  df-bi 197  df-vd1 38786

This theorem is referenced by:  sspwtr  39048  pwtrVD  39059  pwtrrVD  39060  suctrALT2VD  39071  truniALTVD  39114  trintALTVD  39116  suctrALTcfVD  39159