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

Theorem gen11 28388
Description: Virtual deduction generalizing rule for 1 quantifying variable and 1 virtual hypothesis. alrimiv 1617 is gen11 28388 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 28344 . . . 4  |-  ( (.
ph 
->.  ps ).  ->  ( ph  ->  ps ) )
31, 2ax-mp 8 . . 3  |-  ( ph  ->  ps )
43alrimiv 1617 . 2  |-  ( ph  ->  A. x ps )
5 dfvd1impr 28345 . 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 1527   (.wvd1 28337
This theorem is referenced by:  trsspwALT  28592  snssiALTVD  28602  sstrALT2VD  28610  elex2VD  28614  elex22VD  28615  tpid3gVD  28618  trsbcVD  28653  sbcssVD  28659  csbingVD  28660  onfrALTVD  28667  csbsngVD  28669  csbxpgVD  28670  csbrngVD  28672  csbunigVD  28674  csbfv12gALTVD  28675  a9e2eqVD  28683  a9e2ndeqVD  28685  sspwimpVD  28695  sspwimpcfVD  28697
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603
This theorem depends on definitions:  df-bi 177  df-vd1 28338
  Copyright terms: Public domain W3C validator