Theorem gen11 44579

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

Syntax hints:   → wi 4  ∀wal 1538  (   wvd1 44532

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 207  df-vd1 44533

This theorem is referenced by:  trsspwALT  44780  snssiALTVD  44789  sstrALT2VD  44796  elex2VD  44800  elex22VD  44801  tpid3gVD  44804  trsbcVD  44839  sbcssgVD  44845  csbingVD  44846  onfrALTVD  44853  csbsngVD  44855  csbxpgVD  44856  csbrngVD  44858  csbunigVD  44860  csbfv12gALTVD  44861  ax6e2eqVD  44869  ax6e2ndeqVD  44871  sspwimpVD  44881  sspwimpcfVD  44883