Theorem gen11 44641

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

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

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 44595

This theorem is referenced by:  trsspwALT  44842  snssiALTVD  44851  sstrALT2VD  44858  elex2VD  44862  elex22VD  44863  tpid3gVD  44866  trsbcVD  44901  sbcssgVD  44907  csbingVD  44908  onfrALTVD  44915  csbsngVD  44917  csbxpgVD  44918  csbrngVD  44920  csbunigVD  44922  csbfv12gALTVD  44923  ax6e2eqVD  44931  ax6e2ndeqVD  44933  sspwimpVD  44943  sspwimpcfVD  44945