Theorem gen11 45439

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

This proof depends on syntax axioms:   → wi 4  ∀wal 1568  (   wvd1 45392

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943

This proof depends on definitions:  df-bi 210  df-vd1 45393

This theorem is used by:  trsspwALT  45640  snssiALTVD  45649  sstrALT2VD  45656  elex2VD  45660  elex22VD  45661  tpid3gVD  45664  trsbcVD  45699  sbcssgVD  45705  csbingVD  45706  onfrALTVD  45713  csbsngVD  45715  csbxpgVD  45716  csbrngVD  45718  csbunigVD  45720  csbfv12gALTVD  45721  ax6e2eqVD  45729  ax6e2ndeqVD  45731  sspwimpVD  45741  sspwimpcfVD  45743