Theorem gen11 44972

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

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

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 44926

This theorem is referenced by:  trsspwALT  45173  snssiALTVD  45182  sstrALT2VD  45189  elex2VD  45193  elex22VD  45194  tpid3gVD  45197  trsbcVD  45232  sbcssgVD  45238  csbingVD  45239  onfrALTVD  45246  csbsngVD  45248  csbxpgVD  45249  csbrngVD  45251  csbunigVD  45253  csbfv12gALTVD  45254  ax6e2eqVD  45262  ax6e2ndeqVD  45264  sspwimpVD  45274  sspwimpcfVD  45276