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

Theorem gen11 33270
Description: Virtual deduction generalizing rule for 1 quantifying variable and 1 virtual hypothesis. alrimiv 1706 is gen11 33270 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 33220 . . . 4  |-  ( (.
ph 
->.  ps ).  ->  ( ph  ->  ps ) )
31, 2ax-mp 5 . . 3  |-  ( ph  ->  ps )
43alrimiv 1706 . 2  |-  ( ph  ->  A. x ps )
5 dfvd1impr 33221 . 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 1381   (.wvd1 33214
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691
This theorem depends on definitions:  df-bi 185  df-vd1 33215
This theorem is referenced by:  trsspwALT  33484  snssiALTVD  33495  sstrALT2VD  33502  elex2VD  33506  elex22VD  33507  tpid3gVD  33510  trsbcVD  33545  sbcssgVD  33551  csbingVD  33552  onfrALTVD  33559  csbsngVD  33561  csbxpgVD  33562  csbrngVD  33564  csbunigVD  33566  csbfv12gALTVD  33567  ax6e2eqVD  33575  ax6e2ndeqVD  33577  sspwimpVD  33587  sspwimpcfVD  33589
  Copyright terms: Public domain W3C validator