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 44636
Description: Virtual deduction generalizing rule for one quantifying variable and one virtual hypothesis. alrimiv 1927 is gen11 44636 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 44595 . . . 4 ((   𝜑   ▶   𝜓   ) → (𝜑𝜓))
31, 2ax-mp 5 . . 3 (𝜑𝜓)
43alrimiv 1927 . 2 (𝜑 → ∀𝑥𝜓)
5 dfvd1impr 44596 . 2 ((𝜑 → ∀𝑥𝜓) → (   𝜑   ▶   𝑥𝜓   ))
64, 5ax-mp 5 1 (   𝜑   ▶   𝑥𝜓   )
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1538  (   wvd1 44589
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910
This theorem depends on definitions:  df-bi 207  df-vd1 44590
This theorem is referenced by:  trsspwALT  44838  snssiALTVD  44847  sstrALT2VD  44854  elex2VD  44858  elex22VD  44859  tpid3gVD  44862  trsbcVD  44897  sbcssgVD  44903  csbingVD  44904  onfrALTVD  44911  csbsngVD  44913  csbxpgVD  44914  csbrngVD  44916  csbunigVD  44918  csbfv12gALTVD  44919  ax6e2eqVD  44927  ax6e2ndeqVD  44929  sspwimpVD  44939  sspwimpcfVD  44941
  Copyright terms: Public domain W3C validator