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 44614
Description: Virtual deduction generalizing rule for one quantifying variable and one virtual hypothesis. alrimiv 1925 is gen11 44614 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 44573 . . . 4 ((   𝜑   ▶   𝜓   ) → (𝜑𝜓))
31, 2ax-mp 5 . . 3 (𝜑𝜓)
43alrimiv 1925 . 2 (𝜑 → ∀𝑥𝜓)
5 dfvd1impr 44574 . 2 ((𝜑 → ∀𝑥𝜓) → (   𝜑   ▶   𝑥𝜓   ))
64, 5ax-mp 5 1 (   𝜑   ▶   𝑥𝜓   )
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1535  (   wvd1 44567
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908
This theorem depends on definitions:  df-bi 207  df-vd1 44568
This theorem is referenced by:  trsspwALT  44816  snssiALTVD  44825  sstrALT2VD  44832  elex2VD  44836  elex22VD  44837  tpid3gVD  44840  trsbcVD  44875  sbcssgVD  44881  csbingVD  44882  onfrALTVD  44889  csbsngVD  44891  csbxpgVD  44892  csbrngVD  44894  csbunigVD  44896  csbfv12gALTVD  44897  ax6e2eqVD  44905  ax6e2ndeqVD  44907  sspwimpVD  44917  sspwimpcfVD  44919
  Copyright terms: Public domain W3C validator