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 45383
Description: Virtual deduction generalizing rule for one quantifying variable and one virtual hypothesis. alrimiv 1960 is gen11 45383 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 45342 . . . 4 ((   𝜑   ▶   𝜓   ) → (𝜑𝜓))
31, 2ax-mp 5 . . 3 (𝜑𝜓)
43alrimiv 1960 . 2 (𝜑 → ∀𝑥𝜓)
5 dfvd1impr 45343 . 2 ((𝜑 → ∀𝑥𝜓) → (   𝜑   ▶   𝑥𝜓   ))
64, 5ax-mp 5 1 (   𝜑   ▶   𝑥𝜓   )
Colors of variables:    wff setvar class
This proof depends on syntax axioms:  wi 4  wal 1568  (   wvd1 45336
This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943
This proof depends on definitions:  df-bi 210  df-vd1 45337
This theorem is used by:  trsspwALT  45584  snssiALTVD  45593  sstrALT2VD  45600  elex2VD  45604  elex22VD  45605  tpid3gVD  45608  trsbcVD  45643  sbcssgVD  45649  csbingVD  45650  onfrALTVD  45657  csbsngVD  45659  csbxpgVD  45660  csbrngVD  45662  csbunigVD  45664  csbfv12gALTVD  45665  ax6e2eqVD  45673  ax6e2ndeqVD  45675  sspwimpVD  45685  sspwimpcfVD  45687
  Copyright terms: Public domain W3C validator