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 39158
Description: Virtual deduction generalizing rule for one quantifying variable and one virtual hypothesis. alrimiv 1895 is gen11 39158 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 39108 . . . 4 ((   𝜑   ▶   𝜓   ) → (𝜑𝜓))
31, 2ax-mp 5 . . 3 (𝜑𝜓)
43alrimiv 1895 . 2 (𝜑 → ∀𝑥𝜓)
5 dfvd1impr 39109 . 2 ((𝜑 → ∀𝑥𝜓) → (   𝜑   ▶   𝑥𝜓   ))
64, 5ax-mp 5 1 (   𝜑   ▶   𝑥𝜓   )
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1521  (   wvd1 39102
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879
This theorem depends on definitions:  df-bi 197  df-vd1 39103
This theorem is referenced by:  trsspwALT  39362  snssiALTVD  39376  sstrALT2VD  39383  elex2VD  39387  elex22VD  39388  tpid3gVD  39391  trsbcVD  39427  sbcssgVD  39433  csbingVD  39434  onfrALTVD  39441  csbsngVD  39443  csbxpgVD  39444  csbrngVD  39446  csbunigVD  39448  csbfv12gALTVD  39449  ax6e2eqVD  39457  ax6e2ndeqVD  39459  sspwimpVD  39469  sspwimpcfVD  39471
  Copyright terms: Public domain W3C validator