Theorem gen11 39158

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

Syntax hints:   → wi 4  ∀wal 1521  (   wvd1 39102

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879

This theorem depends on definitions:  df-bi 197  df-vd1 39103

This theorem is referenced by:  trsspwALT  39362  snssiALTVD  39376  sstrALT2VD  39383  elex2VD  39387  elex22VD  39388  tpid3gVD  39391  trsbcVD  39427  sbcssgVD  39433  csbingVD  39434  onfrALTVD  39441  csbsngVD  39443  csbxpgVD  39444  csbrngVD  39446  csbunigVD  39448  csbfv12gALTVD  39449  ax6e2eqVD  39457  ax6e2ndeqVD  39459  sspwimpVD  39469  sspwimpcfVD  39471