Theorem gen11 44657

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

Syntax hints:   → wi 4  ∀wal 1539  (   wvd1 44610

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

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

This theorem is referenced by:  trsspwALT  44858  snssiALTVD  44867  sstrALT2VD  44874  elex2VD  44878  elex22VD  44879  tpid3gVD  44882  trsbcVD  44917  sbcssgVD  44923  csbingVD  44924  onfrALTVD  44931  csbsngVD  44933  csbxpgVD  44934  csbrngVD  44936  csbunigVD  44938  csbfv12gALTVD  44939  ax6e2eqVD  44947  ax6e2ndeqVD  44949  sspwimpVD  44959  sspwimpcfVD  44961