Theorem gen11 37862

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

Syntax hints:   → wi 4  ∀wal 1473  (   wvd1 37806

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827

This theorem depends on definitions:  df-bi 196  df-vd1 37807

This theorem is referenced by:  trsspwALT  38067  snssiALTVD  38084  sstrALT2VD  38091  elex2VD  38095  elex22VD  38096  tpid3gVD  38099  trsbcVD  38135  sbcssgVD  38141  csbingVD  38142  onfrALTVD  38149  csbsngVD  38151  csbxpgVD  38152  csbrngVD  38154  csbunigVD  38156  csbfv12gALTVD  38157  ax6e2eqVD  38165  ax6e2ndeqVD  38167  sspwimpVD  38177  sspwimpcfVD  38179