Theorem gen11 44857

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

Syntax hints:   → wi 4  ∀wal 1539  (   wvd1 44810

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

This theorem depends on definitions:  df-bi 207  df-vd1 44811

This theorem is referenced by:  trsspwALT  45058  snssiALTVD  45067  sstrALT2VD  45074  elex2VD  45078  elex22VD  45079  tpid3gVD  45082  trsbcVD  45117  sbcssgVD  45123  csbingVD  45124  onfrALTVD  45131  csbsngVD  45133  csbxpgVD  45134  csbrngVD  45136  csbunigVD  45138  csbfv12gALTVD  45139  ax6e2eqVD  45147  ax6e2ndeqVD  45149  sspwimpVD  45159  sspwimpcfVD  45161