Theorem gen11 42236

Description: Virtual deduction generalizing rule for one quantifying variable and one virtual hypothesis. alrimiv 1930 is gen11 42236 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

Step	Hyp	Ref	Expression
1		gen11.1	. . . 4 ⊢ (   𝜑   ▶   𝜓   )
2		dfvd1imp 42195	. . . 4 ⊢ ((   𝜑   ▶   𝜓   ) → (𝜑 → 𝜓))
3	1, 2	ax-mp 5	. . 3 ⊢ (𝜑 → 𝜓)
4	3	alrimiv 1930	. 2 ⊢ (𝜑 → ∀𝑥𝜓)
5		dfvd1impr 42196	. 2 ⊢ ((𝜑 → ∀𝑥𝜓) → (   𝜑   ▶   ∀𝑥𝜓   ))
6	4, 5	ax-mp 5	1 ⊢ (   𝜑   ▶   ∀𝑥𝜓   )

Syntax hints:   → wi 4  ∀wal 1537  (   wvd1 42189

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913

This theorem depends on definitions:  df-bi 206  df-vd1 42190

This theorem is referenced by:  trsspwALT  42438  snssiALTVD  42447  sstrALT2VD  42454  elex2VD  42458  elex22VD  42459  tpid3gVD  42462  trsbcVD  42497  sbcssgVD  42503  csbingVD  42504  onfrALTVD  42511  csbsngVD  42513  csbxpgVD  42514  csbrngVD  42516  csbunigVD  42518  csbfv12gALTVD  42519  ax6e2eqVD  42527  ax6e2ndeqVD  42529  sspwimpVD  42539  sspwimpcfVD  42541