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 39662
Description: Virtual deduction generalizing rule for one quantifying variable and one virtual hypothesis. alrimiv 2026 is gen11 39662 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 39612 . . . 4 ((   𝜑   ▶   𝜓   ) → (𝜑𝜓))
31, 2ax-mp 5 . . 3 (𝜑𝜓)
43alrimiv 2026 . 2 (𝜑 → ∀𝑥𝜓)
5 dfvd1impr 39613 . 2 ((𝜑 → ∀𝑥𝜓) → (   𝜑   ▶   𝑥𝜓   ))
64, 5ax-mp 5 1 (   𝜑   ▶   𝑥𝜓   )
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1654  (   wvd1 39606
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009
This theorem depends on definitions:  df-bi 199  df-vd1 39607
This theorem is referenced by:  trsspwALT  39865  snssiALTVD  39874  sstrALT2VD  39881  elex2VD  39885  elex22VD  39886  tpid3gVD  39889  trsbcVD  39924  sbcssgVD  39930  csbingVD  39931  onfrALTVD  39938  csbsngVD  39940  csbxpgVD  39941  csbrngVD  39943  csbunigVD  39945  csbfv12gALTVD  39946  ax6e2eqVD  39954  ax6e2ndeqVD  39956  sspwimpVD  39966  sspwimpcfVD  39968
  Copyright terms: Public domain W3C validator