Metamath Proof Explorer


Theorem gen11

Description: Virtual deduction generalizing rule for one quantifying variable and one virtual hypothesis. alrimiv is gen11 without virtual deductions. (Contributed by Alan Sare, 21-Apr-2011) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 gen11.1
 |-  (. ph ->. ps ).
2 dfvd1imp
 |-  ( (. ph ->. ps ). -> ( ph -> ps ) )
3 1 2 ax-mp
 |-  ( ph -> ps )
4 3 alrimiv
 |-  ( ph -> A. x ps )
5 dfvd1impr
 |-  ( ( ph -> A. x ps ) -> (. ph ->. A. x ps ). )
6 4 5 ax-mp
 |-  (. ph ->. A. x ps ).