Theorem gen11 41322

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

Syntax hints:   → wi 4  ∀wal 1536  (   wvd1 41275

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 1911

This theorem depends on definitions:  df-bi 210  df-vd1 41276

This theorem is referenced by:  trsspwALT  41524  snssiALTVD  41533  sstrALT2VD  41540  elex2VD  41544  elex22VD  41545  tpid3gVD  41548  trsbcVD  41583  sbcssgVD  41589  csbingVD  41590  onfrALTVD  41597  csbsngVD  41599  csbxpgVD  41600  csbrngVD  41602  csbunigVD  41604  csbfv12gALTVD  41605  ax6e2eqVD  41613  ax6e2ndeqVD  41615  sspwimpVD  41625  sspwimpcfVD  41627