Users' Mathboxes Mathbox for Alan Sare < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  hbalgVD Structured version   Visualization version   GIF version

Theorem hbalgVD 44925
Description: Virtual deduction proof of hbalg 44575. 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 44575 is hbalgVD 44925 without virtual deductions and was automatically derived from hbalgVD 44925. (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
StepHypRef Expression
1 hba1 2293 . . 3 (∀𝑦(𝜑 → ∀𝑥𝜑) → ∀𝑦𝑦(𝜑 → ∀𝑥𝜑))
2 idn1 44594 . . . . 5 (   𝑦(𝜑 → ∀𝑥𝜑)   ▶   𝑦(𝜑 → ∀𝑥𝜑)   )
3 alim 1810 . . . . 5 (∀𝑦(𝜑 → ∀𝑥𝜑) → (∀𝑦𝜑 → ∀𝑦𝑥𝜑))
42, 3e1a 44647 . . . 4 (   𝑦(𝜑 → ∀𝑥𝜑)   ▶   (∀𝑦𝜑 → ∀𝑦𝑥𝜑)   )
5 ax-11 2157 . . . 4 (∀𝑦𝑥𝜑 → ∀𝑥𝑦𝜑)
6 imim1 83 . . . 4 ((∀𝑦𝜑 → ∀𝑦𝑥𝜑) → ((∀𝑦𝑥𝜑 → ∀𝑥𝑦𝜑) → (∀𝑦𝜑 → ∀𝑥𝑦𝜑)))
74, 5, 6e10 44714 . . 3 (   𝑦(𝜑 → ∀𝑥𝜑)   ▶   (∀𝑦𝜑 → ∀𝑥𝑦𝜑)   )
81, 7gen11nv 44637 . 2 (   𝑦(𝜑 → ∀𝑥𝜑)   ▶   𝑦(∀𝑦𝜑 → ∀𝑥𝑦𝜑)   )
98in1 44591 1 (∀𝑦(𝜑 → ∀𝑥𝜑) → ∀𝑦(∀𝑦𝜑 → ∀𝑥𝑦𝜑))
Colors of variables: wff setvar class
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 2007  ax-10 2141  ax-11 2157  ax-12 2177
This theorem depends on definitions:  df-bi 207  df-or 849  df-ex 1780  df-nf 1784  df-vd1 44590
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator