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 41242
Description: Virtual deduction generalizing rule for one quantifying variable and one virtual hypothesis. alrimiv 1929 is gen11 41242 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 41201 . . . 4 ((   𝜑   ▶   𝜓   ) → (𝜑𝜓))
31, 2ax-mp 5 . . 3 (𝜑𝜓)
43alrimiv 1929 . 2 (𝜑 → ∀𝑥𝜓)
5 dfvd1impr 41202 . 2 ((𝜑 → ∀𝑥𝜓) → (   𝜑   ▶   𝑥𝜓   ))
64, 5ax-mp 5 1 (   𝜑   ▶   𝑥𝜓   )
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1536  (   wvd1 41195
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912
This theorem depends on definitions:  df-bi 210  df-vd1 41196
This theorem is referenced by:  trsspwALT  41444  snssiALTVD  41453  sstrALT2VD  41460  elex2VD  41464  elex22VD  41465  tpid3gVD  41468  trsbcVD  41503  sbcssgVD  41509  csbingVD  41510  onfrALTVD  41517  csbsngVD  41519  csbxpgVD  41520  csbrngVD  41522  csbunigVD  41524  csbfv12gALTVD  41525  ax6e2eqVD  41533  ax6e2ndeqVD  41535  sspwimpVD  41545  sspwimpcfVD  41547
  Copyright terms: Public domain W3C validator