Metamath Proof Explorer


Theorem gen12

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

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

Proof

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