Theorem gen11 45859

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

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

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 1945

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

This theorem is used by:  trsspwALT  46060  snssiALTVD  46069  sstrALT2VD  46076  elex2VD  46080  elex22VD  46081  tpid3gVD  46084  trsbcVD  46119  sbcssgVD  46125  csbingVD  46126  onfrALTVD  46133  csbsngVD  46135  csbxpgVD  46136  csbrngVD  46138  csbunigVD  46140  csbfv12gALTVD  46141  ax6e2eqVD  46149  ax6e2ndeqVD  46151  sspwimpVD  46161  sspwimpcfVD  46163