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

Theorem gen11 36854
Description: Virtual deduction generalizing rule for one quantifying variable and one virtual hypothesis. alrimiv 1763 is gen11 36854 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 36804 . . . 4  |-  ( (.
ph 
->.  ps ).  ->  ( ph  ->  ps ) )
31, 2ax-mp 5 . . 3  |-  ( ph  ->  ps )
43alrimiv 1763 . 2  |-  ( ph  ->  A. x ps )
5 dfvd1impr 36805 . 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 1435   (.wvd1 36798
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748
This theorem depends on definitions:  df-bi 188  df-vd1 36799
This theorem is referenced by:  trsspwALT  37067  snssiALTVD  37084  sstrALT2VD  37091  elex2VD  37095  elex22VD  37096  tpid3gVD  37099  trsbcVD  37135  sbcssgVD  37141  csbingVD  37142  onfrALTVD  37149  csbsngVD  37151  csbxpgVD  37152  csbrngVD  37154  csbunigVD  37156  csbfv12gALTVD  37157  ax6e2eqVD  37165  ax6e2ndeqVD  37167  sspwimpVD  37177  sspwimpcfVD  37179
  Copyright terms: Public domain W3C validator