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

Theorem gen11 28717
Description: Virtual deduction generalizing rule for 1 quantifying variable and 1 virtual hypothesis. alrimiv 1641 is gen11 28717 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 28667 . . . 4  |-  ( (.
ph 
->.  ps ).  ->  ( ph  ->  ps ) )
31, 2ax-mp 8 . . 3  |-  ( ph  ->  ps )
43alrimiv 1641 . 2  |-  ( ph  ->  A. x ps )
5 dfvd1impr 28668 . 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 1549   (.wvd1 28660
This theorem is referenced by:  trsspwALT  28931  snssiALTVD  28939  sstrALT2VD  28946  elex2VD  28950  elex22VD  28951  tpid3gVD  28954  trsbcVD  28989  sbcssVD  28995  csbingVD  28996  onfrALTVD  29003  csbsngVD  29005  csbxpgVD  29006  csbrngVD  29008  csbunigVD  29010  csbfv12gALTVD  29011  a9e2eqVD  29019  a9e2ndeqVD  29021  sspwimpVD  29031  sspwimpcfVD  29033
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626
This theorem depends on definitions:  df-bi 178  df-vd1 28661
  Copyright terms: Public domain W3C validator