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 41848.
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 41848
is hbalgVD 42198 without virtual deductions and was automatically derived
from hbalgVD 42198. (Contributed by Alan Sare, 8-Feb-2014.)
(Proof modification is discouraged.) (New usage is discouraged.)
|
Ref | Expression |
---|---|
hbalgVD | ⊢ (∀𝑦(𝜑 → ∀𝑥𝜑) → ∀𝑦(∀𝑦𝜑 → ∀𝑥∀𝑦𝜑)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hba1 2294 | . . 3 ⊢ (∀𝑦(𝜑 → ∀𝑥𝜑) → ∀𝑦∀𝑦(𝜑 → ∀𝑥𝜑)) | |
2 | idn1 41867 | . . . . 5 ⊢ ( ∀𝑦(𝜑 → ∀𝑥𝜑) ▶ ∀𝑦(𝜑 → ∀𝑥𝜑) ) | |
3 | alim 1818 | . . . . 5 ⊢ (∀𝑦(𝜑 → ∀𝑥𝜑) → (∀𝑦𝜑 → ∀𝑦∀𝑥𝜑)) | |
4 | 2, 3 | e1a 41920 | . . . 4 ⊢ ( ∀𝑦(𝜑 → ∀𝑥𝜑) ▶ (∀𝑦𝜑 → ∀𝑦∀𝑥𝜑) ) |
5 | ax-11 2158 | . . . 4 ⊢ (∀𝑦∀𝑥𝜑 → ∀𝑥∀𝑦𝜑) | |
6 | imim1 83 | . . . 4 ⊢ ((∀𝑦𝜑 → ∀𝑦∀𝑥𝜑) → ((∀𝑦∀𝑥𝜑 → ∀𝑥∀𝑦𝜑) → (∀𝑦𝜑 → ∀𝑥∀𝑦𝜑))) | |
7 | 4, 5, 6 | e10 41987 | . . 3 ⊢ ( ∀𝑦(𝜑 → ∀𝑥𝜑) ▶ (∀𝑦𝜑 → ∀𝑥∀𝑦𝜑) ) |
8 | 1, 7 | gen11nv 41910 | . 2 ⊢ ( ∀𝑦(𝜑 → ∀𝑥𝜑) ▶ ∀𝑦(∀𝑦𝜑 → ∀𝑥∀𝑦𝜑) ) |
9 | 8 | in1 41864 | 1 ⊢ (∀𝑦(𝜑 → ∀𝑥𝜑) → ∀𝑦(∀𝑦𝜑 → ∀𝑥∀𝑦𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1541 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-10 2141 ax-11 2158 ax-12 2175 |
This theorem depends on definitions: df-bi 210 df-or 848 df-ex 1788 df-nf 1792 df-vd1 41863 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |