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

Theorem gen11 44292
Description: Virtual deduction generalizing rule for one quantifying variable and one virtual hypothesis. alrimiv 1923 is gen11 44292 without virtual deductions. (Contributed by Alan Sare, 21-Apr-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
Hypothesis
Ref Expression
gen11.1 (   𝜑   ▶   𝜓   )
Assertion
Ref Expression
gen11 (   𝜑   ▶   𝑥𝜓   )
Distinct variable group:   𝜑,𝑥
Allowed substitution hint:   𝜓(𝑥)

Proof of Theorem gen11
StepHypRef Expression
1 gen11.1 . . . 4 (   𝜑   ▶   𝜓   )
2 dfvd1imp 44251 . . . 4 ((   𝜑   ▶   𝜓   ) → (𝜑𝜓))
31, 2ax-mp 5 . . 3 (𝜑𝜓)
43alrimiv 1923 . 2 (𝜑 → ∀𝑥𝜓)
5 dfvd1impr 44252 . 2 ((𝜑 → ∀𝑥𝜓) → (   𝜑   ▶   𝑥𝜓   ))
64, 5ax-mp 5 1 (   𝜑   ▶   𝑥𝜓   )
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1532  (   wvd1 44245
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906
This theorem depends on definitions:  df-bi 206  df-vd1 44246
This theorem is referenced by:  trsspwALT  44494  snssiALTVD  44503  sstrALT2VD  44510  elex2VD  44514  elex22VD  44515  tpid3gVD  44518  trsbcVD  44553  sbcssgVD  44559  csbingVD  44560  onfrALTVD  44567  csbsngVD  44569  csbxpgVD  44570  csbrngVD  44572  csbunigVD  44574  csbfv12gALTVD  44575  ax6e2eqVD  44583  ax6e2ndeqVD  44585  sspwimpVD  44595  sspwimpcfVD  44597
  Copyright terms: Public domain W3C validator