Theorem gen11 38841

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

Syntax hints:   → wi 4  ∀wal 1481  (   wvd1 38785

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839

This theorem depends on definitions:  df-bi 197  df-vd1 38786

This theorem is referenced by:  trsspwALT  39045  snssiALTVD  39062  sstrALT2VD  39069  elex2VD  39073  elex22VD  39074  tpid3gVD  39077  trsbcVD  39113  sbcssgVD  39119  csbingVD  39120  onfrALTVD  39127  csbsngVD  39129  csbxpgVD  39130  csbrngVD  39132  csbunigVD  39134  csbfv12gALTVD  39135  ax6e2eqVD  39143  ax6e2ndeqVD  39145  sspwimpVD  39155  sspwimpcfVD  39157