Theorem hbalgVD 41246

Description: Virtual deduction proof of hbalg 40896. 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 40896 is hbalgVD 41246 without virtual deductions and was automatically derived from hbalgVD 41246. (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 2301	. . 3 ⊢ (∀𝑦(𝜑 → ∀𝑥𝜑) → ∀𝑦∀𝑦(𝜑 → ∀𝑥𝜑))
2		idn1 40915	. . . . 5 ⊢ (   ∀𝑦(𝜑 → ∀𝑥𝜑)   ▶   ∀𝑦(𝜑 → ∀𝑥𝜑)   )
3		alim 1811	. . . . 5 ⊢ (∀𝑦(𝜑 → ∀𝑥𝜑) → (∀𝑦𝜑 → ∀𝑦∀𝑥𝜑))
4	2, 3	e1a 40968	. . . 4 ⊢ (   ∀𝑦(𝜑 → ∀𝑥𝜑)   ▶   (∀𝑦𝜑 → ∀𝑦∀𝑥𝜑)   )
5		ax-11 2161	. . . 4 ⊢ (∀𝑦∀𝑥𝜑 → ∀𝑥∀𝑦𝜑)
6		imim1 83	. . . 4 ⊢ ((∀𝑦𝜑 → ∀𝑦∀𝑥𝜑) → ((∀𝑦∀𝑥𝜑 → ∀𝑥∀𝑦𝜑) → (∀𝑦𝜑 → ∀𝑥∀𝑦𝜑)))
7	4, 5, 6	e10 41035	. . 3 ⊢ (   ∀𝑦(𝜑 → ∀𝑥𝜑)   ▶   (∀𝑦𝜑 → ∀𝑥∀𝑦𝜑)   )
8	1, 7	gen11nv 40958	. 2 ⊢ (   ∀𝑦(𝜑 → ∀𝑥𝜑)   ▶   ∀𝑦(∀𝑦𝜑 → ∀𝑥∀𝑦𝜑)   )
9	8	in1 40912	1 ⊢ (∀𝑦(𝜑 → ∀𝑥𝜑) → ∀𝑦(∀𝑦𝜑 → ∀𝑥∀𝑦𝜑))

Syntax hints:   → wi 4  ∀wal 1535

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-10 2145  ax-11 2161  ax-12 2177

This theorem depends on definitions:  df-bi 209  df-or 844  df-ex 1781  df-nf 1785  df-vd1 40911

This theorem is referenced by: (None)