Theorem gen11 43377

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

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

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 43331

This theorem is referenced by:  trsspwALT  43579  snssiALTVD  43588  sstrALT2VD  43595  elex2VD  43599  elex22VD  43600  tpid3gVD  43603  trsbcVD  43638  sbcssgVD  43644  csbingVD  43645  onfrALTVD  43652  csbsngVD  43654  csbxpgVD  43655  csbrngVD  43657  csbunigVD  43659  csbfv12gALTVD  43660  ax6e2eqVD  43668  ax6e2ndeqVD  43670  sspwimpVD  43680  sspwimpcfVD  43682