Theorem gen11 40956

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

Syntax hints:   → wi 4  ∀wal 1534  (   wvd1 40909

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

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

This theorem is referenced by:  trsspwALT  41158  snssiALTVD  41167  sstrALT2VD  41174  elex2VD  41178  elex22VD  41179  tpid3gVD  41182  trsbcVD  41217  sbcssgVD  41223  csbingVD  41224  onfrALTVD  41231  csbsngVD  41233  csbxpgVD  41234  csbrngVD  41236  csbunigVD  41238  csbfv12gALTVD  41239  ax6e2eqVD  41247  ax6e2ndeqVD  41249  sspwimpVD  41259  sspwimpcfVD  41261