Theorem gen11 45584

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

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

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 45538

This theorem is used by:  trsspwALT  45785  snssiALTVD  45794  sstrALT2VD  45801  elex2VD  45805  elex22VD  45806  tpid3gVD  45809  trsbcVD  45844  sbcssgVD  45850  csbingVD  45851  onfrALTVD  45858  csbsngVD  45860  csbxpgVD  45861  csbrngVD  45863  csbunigVD  45865  csbfv12gALTVD  45866  ax6e2eqVD  45874  ax6e2ndeqVD  45876  sspwimpVD  45886  sspwimpcfVD  45888