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 38661
Description: Virtual deduction generalizing rule for one quantifying variable and one virtual hypothesis. alrimiv 1853 is gen11 38661 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 38611 . . . 4 ((   𝜑   ▶   𝜓   ) → (𝜑𝜓))
31, 2ax-mp 5 . . 3 (𝜑𝜓)
43alrimiv 1853 . 2 (𝜑 → ∀𝑥𝜓)
5 dfvd1impr 38612 . 2 ((𝜑 → ∀𝑥𝜓) → (   𝜑   ▶   𝑥𝜓   ))
64, 5ax-mp 5 1 (   𝜑   ▶   𝑥𝜓   )
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1479  (   wvd1 38605
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837
This theorem depends on definitions:  df-bi 197  df-vd1 38606
This theorem is referenced by:  trsspwALT  38865  snssiALTVD  38882  sstrALT2VD  38889  elex2VD  38893  elex22VD  38894  tpid3gVD  38897  trsbcVD  38933  sbcssgVD  38939  csbingVD  38940  onfrALTVD  38947  csbsngVD  38949  csbxpgVD  38950  csbrngVD  38952  csbunigVD  38954  csbfv12gALTVD  38955  ax6e2eqVD  38963  ax6e2ndeqVD  38965  sspwimpVD  38975  sspwimpcfVD  38977
  Copyright terms: Public domain W3C validator