Theorem gen11 44606

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

Syntax hints:   → wi 4  ∀wal 1538  (   wvd1 44559

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

This theorem depends on definitions:  df-bi 207  df-vd1 44560

This theorem is referenced by:  trsspwALT  44807  snssiALTVD  44816  sstrALT2VD  44823  elex2VD  44827  elex22VD  44828  tpid3gVD  44831  trsbcVD  44866  sbcssgVD  44872  csbingVD  44873  onfrALTVD  44880  csbsngVD  44882  csbxpgVD  44883  csbrngVD  44885  csbunigVD  44887  csbfv12gALTVD  44888  ax6e2eqVD  44896  ax6e2ndeqVD  44898  sspwimpVD  44908  sspwimpcfVD  44910