Theorem gen11 45365

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

This proof depends on syntax axioms:   → wi 4  ∀wal 1568  (   wvd1 45318

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943

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

This theorem is used by:  trsspwALT  45566  snssiALTVD  45575  sstrALT2VD  45582  elex2VD  45586  elex22VD  45587  tpid3gVD  45590  trsbcVD  45625  sbcssgVD  45631  csbingVD  45632  onfrALTVD  45639  csbsngVD  45641  csbxpgVD  45642  csbrngVD  45644  csbunigVD  45646  csbfv12gALTVD  45647  ax6e2eqVD  45655  ax6e2ndeqVD  45657  sspwimpVD  45667  sspwimpcfVD  45669