Theorem gen11 42125

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

Syntax hints:   → wi 4  ∀wal 1537  (   wvd1 42078

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914

This theorem depends on definitions:  df-bi 206  df-vd1 42079

This theorem is referenced by:  trsspwALT  42327  snssiALTVD  42336  sstrALT2VD  42343  elex2VD  42347  elex22VD  42348  tpid3gVD  42351  trsbcVD  42386  sbcssgVD  42392  csbingVD  42393  onfrALTVD  42400  csbsngVD  42402  csbxpgVD  42403  csbrngVD  42405  csbunigVD  42407  csbfv12gALTVD  42408  ax6e2eqVD  42416  ax6e2ndeqVD  42418  sspwimpVD  42428  sspwimpcfVD  42430