Theorem hbalgVD 44887

Description: Virtual deduction proof of hbalg 44538. 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 44538 is hbalgVD 44887 without virtual deductions and was automatically derived from hbalgVD 44887. (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 2293	. . 3 ⊢ (∀𝑦(𝜑 → ∀𝑥𝜑) → ∀𝑦∀𝑦(𝜑 → ∀𝑥𝜑))
2		idn1 44557	. . . . 5 ⊢ (   ∀𝑦(𝜑 → ∀𝑥𝜑)   ▶   ∀𝑦(𝜑 → ∀𝑥𝜑)   )
3		alim 1810	. . . . 5 ⊢ (∀𝑦(𝜑 → ∀𝑥𝜑) → (∀𝑦𝜑 → ∀𝑦∀𝑥𝜑))
4	2, 3	e1a 44610	. . . 4 ⊢ (   ∀𝑦(𝜑 → ∀𝑥𝜑)   ▶   (∀𝑦𝜑 → ∀𝑦∀𝑥𝜑)   )
5		ax-11 2158	. . . 4 ⊢ (∀𝑦∀𝑥𝜑 → ∀𝑥∀𝑦𝜑)
6		imim1 83	. . . 4 ⊢ ((∀𝑦𝜑 → ∀𝑦∀𝑥𝜑) → ((∀𝑦∀𝑥𝜑 → ∀𝑥∀𝑦𝜑) → (∀𝑦𝜑 → ∀𝑥∀𝑦𝜑)))
7	4, 5, 6	e10 44677	. . 3 ⊢ (   ∀𝑦(𝜑 → ∀𝑥𝜑)   ▶   (∀𝑦𝜑 → ∀𝑥∀𝑦𝜑)   )
8	1, 7	gen11nv 44600	. 2 ⊢ (   ∀𝑦(𝜑 → ∀𝑥𝜑)   ▶   ∀𝑦(∀𝑦𝜑 → ∀𝑥∀𝑦𝜑)   )
9	8	in1 44554	1 ⊢ (∀𝑦(𝜑 → ∀𝑥𝜑) → ∀𝑦(∀𝑦𝜑 → ∀𝑥∀𝑦𝜑))

Syntax hints:   → wi 4  ∀wal 1538

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  ax-6 1967  ax-7 2008  ax-10 2142  ax-11 2158  ax-12 2178

This theorem depends on definitions:  df-bi 207  df-or 848  df-ex 1780  df-nf 1784  df-vd1 44553

This theorem is referenced by: (None)