Theorem gen11 45043

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

Syntax hints:   → wi 4  ∀wal 1540  (   wvd1 44996

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912

This theorem depends on definitions:  df-bi 207  df-vd1 44997

This theorem is referenced by:  trsspwALT  45244  snssiALTVD  45253  sstrALT2VD  45260  elex2VD  45264  elex22VD  45265  tpid3gVD  45268  trsbcVD  45303  sbcssgVD  45309  csbingVD  45310  onfrALTVD  45317  csbsngVD  45319  csbxpgVD  45320  csbrngVD  45322  csbunigVD  45324  csbfv12gALTVD  45325  ax6e2eqVD  45333  ax6e2ndeqVD  45335  sspwimpVD  45345  sspwimpcfVD  45347