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 42204
Description: Virtual deduction generalizing rule for one quantifying variable and one virtual hypothesis. alrimiv 1934 is gen11 42204 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 42163 . . . 4 ((   𝜑   ▶   𝜓   ) → (𝜑𝜓))
31, 2ax-mp 5 . . 3 (𝜑𝜓)
43alrimiv 1934 . 2 (𝜑 → ∀𝑥𝜓)
5 dfvd1impr 42164 . 2 ((𝜑 → ∀𝑥𝜓) → (   𝜑   ▶   𝑥𝜓   ))
64, 5ax-mp 5 1 (   𝜑   ▶   𝑥𝜓   )
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1540  (   wvd1 42157
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917
This theorem depends on definitions:  df-bi 206  df-vd1 42158
This theorem is referenced by:  trsspwALT  42406  snssiALTVD  42415  sstrALT2VD  42422  elex2VD  42426  elex22VD  42427  tpid3gVD  42430  trsbcVD  42465  sbcssgVD  42471  csbingVD  42472  onfrALTVD  42479  csbsngVD  42481  csbxpgVD  42482  csbrngVD  42484  csbunigVD  42486  csbfv12gALTVD  42487  ax6e2eqVD  42495  ax6e2ndeqVD  42497  sspwimpVD  42507  sspwimpcfVD  42509
  Copyright terms: Public domain W3C validator