Theorem gen11 45189

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

Syntax hints:   → wi 4  ∀wal 1558  (   wvd1 45142

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930

This theorem depends on definitions:  df-bi 209  df-vd1 45143

This theorem is referenced by:  trsspwALT  45390  snssiALTVD  45399  sstrALT2VD  45406  elex2VD  45410  elex22VD  45411  tpid3gVD  45414  trsbcVD  45449  sbcssgVD  45455  csbingVD  45456  onfrALTVD  45463  csbsngVD  45465  csbxpgVD  45466  csbrngVD  45468  csbunigVD  45470  csbfv12gALTVD  45471  ax6e2eqVD  45479  ax6e2ndeqVD  45481  sspwimpVD  45491  sspwimpcfVD  45493