Theorem gen11 44799

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

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

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 44753

This theorem is referenced by:  trsspwALT  45000  snssiALTVD  45009  sstrALT2VD  45016  elex2VD  45020  elex22VD  45021  tpid3gVD  45024  trsbcVD  45059  sbcssgVD  45065  csbingVD  45066  onfrALTVD  45073  csbsngVD  45075  csbxpgVD  45076  csbrngVD  45078  csbunigVD  45080  csbfv12gALTVD  45081  ax6e2eqVD  45089  ax6e2ndeqVD  45091  sspwimpVD  45101  sspwimpcfVD  45103