Theorem gen11 45060

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

Syntax hints:   → wi 4  ∀wal 1545  (   wvd1 45013

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917

This theorem depends on definitions:  df-bi 208  df-vd1 45014

This theorem is referenced by:  trsspwALT  45261  snssiALTVD  45270  sstrALT2VD  45277  elex2VD  45281  elex22VD  45282  tpid3gVD  45285  trsbcVD  45320  sbcssgVD  45326  csbingVD  45327  onfrALTVD  45334  csbsngVD  45336  csbxpgVD  45337  csbrngVD  45339  csbunigVD  45341  csbfv12gALTVD  45342  ax6e2eqVD  45350  ax6e2ndeqVD  45352  sspwimpVD  45362  sspwimpcfVD  45364