![]() |
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 43618.
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 43618
is hbalgVD 43968 without virtual deductions and was automatically derived
from hbalgVD 43968. (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 43637 | . . . . 5 ⊢ ( ∀𝑦(𝜑 → ∀𝑥𝜑) ▶ ∀𝑦(𝜑 → ∀𝑥𝜑) ) | |
3 | alim 1812 | . . . . 5 ⊢ (∀𝑦(𝜑 → ∀𝑥𝜑) → (∀𝑦𝜑 → ∀𝑦∀𝑥𝜑)) | |
4 | 2, 3 | e1a 43690 | . . . 4 ⊢ ( ∀𝑦(𝜑 → ∀𝑥𝜑) ▶ (∀𝑦𝜑 → ∀𝑦∀𝑥𝜑) ) |
5 | ax-11 2154 | . . . 4 ⊢ (∀𝑦∀𝑥𝜑 → ∀𝑥∀𝑦𝜑) | |
6 | imim1 83 | . . . 4 ⊢ ((∀𝑦𝜑 → ∀𝑦∀𝑥𝜑) → ((∀𝑦∀𝑥𝜑 → ∀𝑥∀𝑦𝜑) → (∀𝑦𝜑 → ∀𝑥∀𝑦𝜑))) | |
7 | 4, 5, 6 | e10 43757 | . . 3 ⊢ ( ∀𝑦(𝜑 → ∀𝑥𝜑) ▶ (∀𝑦𝜑 → ∀𝑥∀𝑦𝜑) ) |
8 | 1, 7 | gen11nv 43680 | . 2 ⊢ ( ∀𝑦(𝜑 → ∀𝑥𝜑) ▶ ∀𝑦(∀𝑦𝜑 → ∀𝑥∀𝑦𝜑) ) |
9 | 8 | in1 43634 | 1 ⊢ (∀𝑦(𝜑 → ∀𝑥𝜑) → ∀𝑦(∀𝑦𝜑 → ∀𝑥∀𝑦𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1539 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-10 2137 ax-11 2154 ax-12 2171 |
This theorem depends on definitions: df-bi 206 df-or 846 df-ex 1782 df-nf 1786 df-vd1 43633 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |