Theorem gen11 44587

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

Syntax hints:   → wi 4  ∀wal 1535  (   wvd1 44540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909

This theorem depends on definitions:  df-bi 207  df-vd1 44541

This theorem is referenced by:  trsspwALT  44789  snssiALTVD  44798  sstrALT2VD  44805  elex2VD  44809  elex22VD  44810  tpid3gVD  44813  trsbcVD  44848  sbcssgVD  44854  csbingVD  44855  onfrALTVD  44862  csbsngVD  44864  csbxpgVD  44865  csbrngVD  44867  csbunigVD  44869  csbfv12gALTVD  44870  ax6e2eqVD  44878  ax6e2ndeqVD  44880  sspwimpVD  44890  sspwimpcfVD  44892