Theorem gen11 45064

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

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

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 45018

This theorem is referenced by:  trsspwALT  45265  snssiALTVD  45274  sstrALT2VD  45281  elex2VD  45285  elex22VD  45286  tpid3gVD  45289  trsbcVD  45324  sbcssgVD  45330  csbingVD  45331  onfrALTVD  45338  csbsngVD  45340  csbxpgVD  45341  csbrngVD  45343  csbunigVD  45345  csbfv12gALTVD  45346  ax6e2eqVD  45354  ax6e2ndeqVD  45356  sspwimpVD  45366  sspwimpcfVD  45368