| 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 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.)
|
| Ref | Expression |
|---|---|
| hbalgVD | ⊢ (∀𝑦(𝜑 → ∀𝑥𝜑) → ∀𝑦(∀𝑦𝜑 → ∀𝑥∀𝑦𝜑)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | hba1 2293 | . . 3 ⊢ (∀𝑦(𝜑 → ∀𝑥𝜑) → ∀𝑦∀𝑦(𝜑 → ∀𝑥𝜑)) | |
| 2 | idn1 44594 | . . . . 5 ⊢ ( ∀𝑦(𝜑 → ∀𝑥𝜑) ▶ ∀𝑦(𝜑 → ∀𝑥𝜑) ) | |
| 3 | alim 1810 | . . . . 5 ⊢ (∀𝑦(𝜑 → ∀𝑥𝜑) → (∀𝑦𝜑 → ∀𝑦∀𝑥𝜑)) | |
| 4 | 2, 3 | e1a 44647 | . . . 4 ⊢ ( ∀𝑦(𝜑 → ∀𝑥𝜑) ▶ (∀𝑦𝜑 → ∀𝑦∀𝑥𝜑) ) |
| 5 | ax-11 2157 | . . . 4 ⊢ (∀𝑦∀𝑥𝜑 → ∀𝑥∀𝑦𝜑) | |
| 6 | imim1 83 | . . . 4 ⊢ ((∀𝑦𝜑 → ∀𝑦∀𝑥𝜑) → ((∀𝑦∀𝑥𝜑 → ∀𝑥∀𝑦𝜑) → (∀𝑦𝜑 → ∀𝑥∀𝑦𝜑))) | |
| 7 | 4, 5, 6 | e10 44714 | . . 3 ⊢ ( ∀𝑦(𝜑 → ∀𝑥𝜑) ▶ (∀𝑦𝜑 → ∀𝑥∀𝑦𝜑) ) |
| 8 | 1, 7 | gen11nv 44637 | . 2 ⊢ ( ∀𝑦(𝜑 → ∀𝑥𝜑) ▶ ∀𝑦(∀𝑦𝜑 → ∀𝑥∀𝑦𝜑) ) |
| 9 | 8 | in1 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 |