Theorem gen11 45216

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

Syntax hints:   → wi 4  ∀wal 1565  (   wvd1 45169

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937

This theorem depends on definitions:  df-bi 210  df-vd1 45170

This theorem is referenced by:  trsspwALT  45417  snssiALTVD  45426  sstrALT2VD  45433  elex2VD  45437  elex22VD  45438  tpid3gVD  45441  trsbcVD  45476  sbcssgVD  45482  csbingVD  45483  onfrALTVD  45490  csbsngVD  45492  csbxpgVD  45493  csbrngVD  45495  csbunigVD  45497  csbfv12gALTVD  45498  ax6e2eqVD  45506  ax6e2ndeqVD  45508  sspwimpVD  45518  sspwimpcfVD  45520