Users' Mathboxes Mathbox for Alan Sare < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  gen11 Unicode version

Theorem gen11 28693
Description: Virtual deduction generalizing rule for 1 quantifying variable and 1 virtual hypothesis. alrimiv 1621 is gen11 28693 without virtual deductions. (Contributed by Alan Sare, 21-Apr-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
Hypothesis
Ref Expression
gen11.1  |-  (. ph  ->.  ps
).
Assertion
Ref Expression
gen11  |-  (. ph  ->.  A. x ps ).
Distinct variable group:    ph, x
Allowed substitution hint:    ps( x)

Proof of Theorem gen11
StepHypRef Expression
1 gen11.1 . . . 4  |-  (. ph  ->.  ps
).
2 dfvd1imp 28643 . . . 4  |-  ( (.
ph 
->.  ps ).  ->  ( ph  ->  ps ) )
31, 2ax-mp 8 . . 3  |-  ( ph  ->  ps )
43alrimiv 1621 . 2  |-  ( ph  ->  A. x ps )
5 dfvd1impr 28644 . 2  |-  ( (
ph  ->  A. x ps )  ->  (. ph  ->.  A. x ps ). )
64, 5ax-mp 8 1  |-  (. ph  ->.  A. x ps ).
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1530   (.wvd1 28636
This theorem is referenced by:  trsspwALT  28908  snssiALTVD  28918  sstrALT2VD  28926  elex2VD  28930  elex22VD  28931  tpid3gVD  28934  trsbcVD  28969  sbcssVD  28975  csbingVD  28976  onfrALTVD  28983  csbsngVD  28985  csbxpgVD  28986  csbrngVD  28988  csbunigVD  28990  csbfv12gALTVD  28991  a9e2eqVD  28999  a9e2ndeqVD  29001  sspwimpVD  29011  sspwimpcfVD  29013
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606
This theorem depends on definitions:  df-bi 177  df-vd1 28637
  Copyright terms: Public domain W3C validator