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 39527
Description: Virtual deduction generalizing rule for one quantifying variable and one virtual hypothesis. alrimiv 2022 is gen11 39527 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 39477 . . . 4 ((   𝜑   ▶   𝜓   ) → (𝜑𝜓))
31, 2ax-mp 5 . . 3 (𝜑𝜓)
43alrimiv 2022 . 2 (𝜑 → ∀𝑥𝜓)
5 dfvd1impr 39478 . 2 ((𝜑 → ∀𝑥𝜓) → (   𝜑   ▶   𝑥𝜓   ))
64, 5ax-mp 5 1 (   𝜑   ▶   𝑥𝜓   )
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1650  (   wvd1 39471
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005
This theorem depends on definitions:  df-bi 198  df-vd1 39472
This theorem is referenced by:  trsspwALT  39730  snssiALTVD  39739  sstrALT2VD  39746  elex2VD  39750  elex22VD  39751  tpid3gVD  39754  trsbcVD  39789  sbcssgVD  39795  csbingVD  39796  onfrALTVD  39803  csbsngVD  39805  csbxpgVD  39806  csbrngVD  39808  csbunigVD  39810  csbfv12gALTVD  39811  ax6e2eqVD  39819  ax6e2ndeqVD  39821  sspwimpVD  39831  sspwimpcfVD  39833
  Copyright terms: Public domain W3C validator