Theorem gen11 45383

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

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

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 45337

This theorem is used by:  trsspwALT  45584  snssiALTVD  45593  sstrALT2VD  45600  elex2VD  45604  elex22VD  45605  tpid3gVD  45608  trsbcVD  45643  sbcssgVD  45649  csbingVD  45650  onfrALTVD  45657  csbsngVD  45659  csbxpgVD  45660  csbrngVD  45662  csbunigVD  45664  csbfv12gALTVD  45665  ax6e2eqVD  45673  ax6e2ndeqVD  45675  sspwimpVD  45685  sspwimpcfVD  45687