Theorem gen11 45325

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

Syntax hints:   → wi 4  ∀wal 1568  (   wvd1 45278

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

This theorem depends on definitions:  df-bi 210  df-vd1 45279

This theorem is referenced by:  trsspwALT  45526  snssiALTVD  45535  sstrALT2VD  45542  elex2VD  45546  elex22VD  45547  tpid3gVD  45550  trsbcVD  45585  sbcssgVD  45591  csbingVD  45592  onfrALTVD  45599  csbsngVD  45601  csbxpgVD  45602  csbrngVD  45604  csbunigVD  45606  csbfv12gALTVD  45607  ax6e2eqVD  45615  ax6e2ndeqVD  45617  sspwimpVD  45627  sspwimpcfVD  45629