Theorem gen11 45707

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

This proof depends on syntax axioms:   → wi 4  ∀wal 1567  (   wvd1 45660

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942

This proof depends on definitions:  df-bi 210  df-vd1 45661

This theorem is used by:  trsspwALT  45908  snssiALTVD  45917  sstrALT2VD  45924  elex2VD  45928  elex22VD  45929  tpid3gVD  45932  trsbcVD  45967  sbcssgVD  45973  csbingVD  45974  onfrALTVD  45981  csbsngVD  45983  csbxpgVD  45984  csbrngVD  45986  csbunigVD  45988  csbfv12gALTVD  45989  ax6e2eqVD  45997  ax6e2ndeqVD  45999  sspwimpVD  46009  sspwimpcfVD  46011