Theorem gen11 44600

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

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

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 44554

This theorem is referenced by:  trsspwALT  44801  snssiALTVD  44810  sstrALT2VD  44817  elex2VD  44821  elex22VD  44822  tpid3gVD  44825  trsbcVD  44860  sbcssgVD  44866  csbingVD  44867  onfrALTVD  44874  csbsngVD  44876  csbxpgVD  44877  csbrngVD  44879  csbunigVD  44881  csbfv12gALTVD  44882  ax6e2eqVD  44890  ax6e2ndeqVD  44892  sspwimpVD  44902  sspwimpcfVD  44904