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

Theorem gen11 37037
Description: Virtual deduction generalizing rule for one quantifying variable and one virtual hypothesis. alrimiv 1783 is gen11 37037 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 36987 . . . 4  |-  ( (.
ph 
->.  ps ).  ->  ( ph  ->  ps ) )
31, 2ax-mp 5 . . 3  |-  ( ph  ->  ps )
43alrimiv 1783 . 2  |-  ( ph  ->  A. x ps )
5 dfvd1impr 36988 . 2  |-  ( (
ph  ->  A. x ps )  ->  (. ph  ->.  A. x ps ). )
64, 5ax-mp 5 1  |-  (. ph  ->.  A. x ps ).
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   A.wal 1452   (.wvd1 36981
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768
This theorem depends on definitions:  df-bi 190  df-vd1 36982
This theorem is referenced by:  trsspwALT  37245  snssiALTVD  37262  sstrALT2VD  37269  elex2VD  37273  elex22VD  37274  tpid3gVD  37277  trsbcVD  37313  sbcssgVD  37319  csbingVD  37320  onfrALTVD  37327  csbsngVD  37329  csbxpgVD  37330  csbrngVD  37332  csbunigVD  37334  csbfv12gALTVD  37335  ax6e2eqVD  37343  ax6e2ndeqVD  37345  sspwimpVD  37355  sspwimpcfVD  37357
  Copyright terms: Public domain W3C validator