Theorem gen11 40957

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

Syntax hints:   → wi 4  ∀wal 1535  (   wvd1 40910

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 209  df-vd1 40911

This theorem is referenced by:  trsspwALT  41159  snssiALTVD  41168  sstrALT2VD  41175  elex2VD  41179  elex22VD  41180  tpid3gVD  41183  trsbcVD  41218  sbcssgVD  41224  csbingVD  41225  onfrALTVD  41232  csbsngVD  41234  csbxpgVD  41235  csbrngVD  41237  csbunigVD  41239  csbfv12gALTVD  41240  ax6e2eqVD  41248  ax6e2ndeqVD  41250  sspwimpVD  41260  sspwimpcfVD  41262