Theorem gen11 43363

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

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

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 1914

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

This theorem is referenced by:  trsspwALT  43565  snssiALTVD  43574  sstrALT2VD  43581  elex2VD  43585  elex22VD  43586  tpid3gVD  43589  trsbcVD  43624  sbcssgVD  43630  csbingVD  43631  onfrALTVD  43638  csbsngVD  43640  csbxpgVD  43641  csbrngVD  43643  csbunigVD  43645  csbfv12gALTVD  43646  ax6e2eqVD  43654  ax6e2ndeqVD  43656  sspwimpVD  43666  sspwimpcfVD  43668