Mathbox for Alan Sare |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > hbalgVD | Structured version Visualization version GIF version |
Description: Virtual deduction proof of hbalg 42504.
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 42504
is hbalgVD 42854 without virtual deductions and was automatically derived
from hbalgVD 42854. (Contributed by Alan Sare, 8-Feb-2014.)
(Proof modification is discouraged.) (New usage is discouraged.)
|
Ref | Expression |
---|---|
hbalgVD | ⊢ (∀𝑦(𝜑 → ∀𝑥𝜑) → ∀𝑦(∀𝑦𝜑 → ∀𝑥∀𝑦𝜑)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hba1 2289 | . . 3 ⊢ (∀𝑦(𝜑 → ∀𝑥𝜑) → ∀𝑦∀𝑦(𝜑 → ∀𝑥𝜑)) | |
2 | idn1 42523 | . . . . 5 ⊢ ( ∀𝑦(𝜑 → ∀𝑥𝜑) ▶ ∀𝑦(𝜑 → ∀𝑥𝜑) ) | |
3 | alim 1811 | . . . . 5 ⊢ (∀𝑦(𝜑 → ∀𝑥𝜑) → (∀𝑦𝜑 → ∀𝑦∀𝑥𝜑)) | |
4 | 2, 3 | e1a 42576 | . . . 4 ⊢ ( ∀𝑦(𝜑 → ∀𝑥𝜑) ▶ (∀𝑦𝜑 → ∀𝑦∀𝑥𝜑) ) |
5 | ax-11 2153 | . . . 4 ⊢ (∀𝑦∀𝑥𝜑 → ∀𝑥∀𝑦𝜑) | |
6 | imim1 83 | . . . 4 ⊢ ((∀𝑦𝜑 → ∀𝑦∀𝑥𝜑) → ((∀𝑦∀𝑥𝜑 → ∀𝑥∀𝑦𝜑) → (∀𝑦𝜑 → ∀𝑥∀𝑦𝜑))) | |
7 | 4, 5, 6 | e10 42643 | . . 3 ⊢ ( ∀𝑦(𝜑 → ∀𝑥𝜑) ▶ (∀𝑦𝜑 → ∀𝑥∀𝑦𝜑) ) |
8 | 1, 7 | gen11nv 42566 | . 2 ⊢ ( ∀𝑦(𝜑 → ∀𝑥𝜑) ▶ ∀𝑦(∀𝑦𝜑 → ∀𝑥∀𝑦𝜑) ) |
9 | 8 | in1 42520 | 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 1796 ax-4 1810 ax-5 1912 ax-6 1970 ax-7 2010 ax-10 2136 ax-11 2153 ax-12 2170 |
This theorem depends on definitions: df-bi 206 df-or 845 df-ex 1781 df-nf 1785 df-vd1 42519 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |