Theorem hbalgVD 43437

Description: Virtual deduction proof of hbalg 43087. The following User's Proof is a Virtual Deduction proof completed automatically by the tools program completeusersproof.cmd, which invokes Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. hbalg 43087 is hbalgVD 43437 without virtual deductions and was automatically derived from hbalgVD 43437. (Contributed by Alan Sare, 8-Feb-2014.) (Proof modification is discouraged.) (New usage is discouraged.)

1::	⊢ (   ∀𝑦(𝜑 → ∀𝑥𝜑)   ▶   ∀𝑦(𝜑 → ∀𝑥𝜑)   )
2:1:	⊢ (   ∀𝑦(𝜑 → ∀𝑥𝜑)   ▶   (∀𝑦𝜑 → ∀𝑦∀𝑥𝜑)   )
3::	⊢ (∀𝑦∀𝑥𝜑 → ∀𝑥∀𝑦𝜑)
4:2,3:	⊢ (   ∀𝑦(𝜑 → ∀𝑥𝜑)   ▶   (∀𝑦𝜑 → ∀𝑥∀𝑦𝜑)   )
5::	⊢ (∀𝑦(𝜑 → ∀𝑥𝜑) → ∀𝑦∀𝑦( 𝜑 → ∀𝑥𝜑))
6:5,4:	⊢ (   ∀𝑦(𝜑 → ∀𝑥𝜑)   ▶   ∀𝑦(∀ 𝑦𝜑 → ∀𝑥∀𝑦𝜑)   )
qed:6:	⊢ (∀𝑦(𝜑 → ∀𝑥𝜑) → ∀𝑦(∀𝑦 𝜑 → ∀𝑥∀𝑦𝜑))

Assertion

Ref	Expression
hbalgVD	⊢ (∀𝑦(𝜑 → ∀𝑥𝜑) → ∀𝑦(∀𝑦𝜑 → ∀𝑥∀𝑦𝜑))

Proof of Theorem hbalgVD

Step	Hyp	Ref	Expression
1		hba1 2289	. . 3 ⊢ (∀𝑦(𝜑 → ∀𝑥𝜑) → ∀𝑦∀𝑦(𝜑 → ∀𝑥𝜑))
2		idn1 43106	. . . . 5 ⊢ (   ∀𝑦(𝜑 → ∀𝑥𝜑)   ▶   ∀𝑦(𝜑 → ∀𝑥𝜑)   )
3		alim 1812	. . . . 5 ⊢ (∀𝑦(𝜑 → ∀𝑥𝜑) → (∀𝑦𝜑 → ∀𝑦∀𝑥𝜑))
4	2, 3	e1a 43159	. . . 4 ⊢ (   ∀𝑦(𝜑 → ∀𝑥𝜑)   ▶   (∀𝑦𝜑 → ∀𝑦∀𝑥𝜑)   )
5		ax-11 2154	. . . 4 ⊢ (∀𝑦∀𝑥𝜑 → ∀𝑥∀𝑦𝜑)
6		imim1 83	. . . 4 ⊢ ((∀𝑦𝜑 → ∀𝑦∀𝑥𝜑) → ((∀𝑦∀𝑥𝜑 → ∀𝑥∀𝑦𝜑) → (∀𝑦𝜑 → ∀𝑥∀𝑦𝜑)))
7	4, 5, 6	e10 43226	. . 3 ⊢ (   ∀𝑦(𝜑 → ∀𝑥𝜑)   ▶   (∀𝑦𝜑 → ∀𝑥∀𝑦𝜑)   )
8	1, 7	gen11nv 43149	. 2 ⊢ (   ∀𝑦(𝜑 → ∀𝑥𝜑)   ▶   ∀𝑦(∀𝑦𝜑 → ∀𝑥∀𝑦𝜑)   )
9	8	in1 43103	1 ⊢ (∀𝑦(𝜑 → ∀𝑥𝜑) → ∀𝑦(∀𝑦𝜑 → ∀𝑥∀𝑦𝜑))

Syntax hints:   → wi 4  ∀wal 1539

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-10 2137  ax-11 2154  ax-12 2171

This theorem depends on definitions:  df-bi 206  df-or 846  df-ex 1782  df-nf 1786  df-vd1 43102

This theorem is referenced by: (None)