Theorem gen11 42204

Description: Virtual deduction generalizing rule for one quantifying variable and one virtual hypothesis. alrimiv 1934 is gen11 42204 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 42163	. . . 4 ⊢ ((   𝜑   ▶   𝜓   ) → (𝜑 → 𝜓))
3	1, 2	ax-mp 5	. . 3 ⊢ (𝜑 → 𝜓)
4	3	alrimiv 1934	. 2 ⊢ (𝜑 → ∀𝑥𝜓)
5		dfvd1impr 42164	. 2 ⊢ ((𝜑 → ∀𝑥𝜓) → (   𝜑   ▶   ∀𝑥𝜓   ))
6	4, 5	ax-mp 5	1 ⊢ (   𝜑   ▶   ∀𝑥𝜓   )

Syntax hints:   → wi 4  ∀wal 1540  (   wvd1 42157

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917

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

This theorem is referenced by:  trsspwALT  42406  snssiALTVD  42415  sstrALT2VD  42422  elex2VD  42426  elex22VD  42427  tpid3gVD  42430  trsbcVD  42465  sbcssgVD  42471  csbingVD  42472  onfrALTVD  42479  csbsngVD  42481  csbxpgVD  42482  csbrngVD  42484  csbunigVD  42486  csbfv12gALTVD  42487  ax6e2eqVD  42495  ax6e2ndeqVD  42497  sspwimpVD  42507  sspwimpcfVD  42509