Proof of Theorem oath1
| Step | Hyp | Ref
| Expression |
|---|
| 1 | | oaliii 1001 |
. . . 4
((a →2 b) ∩ ((b
∪ c)⊥ ∪ ((a →2 b) ∩ (a
→2 c)))) = ((a →2 c) ∩ ((b
∪ c)⊥ ∪ ((a →2 b) ∩ (a
→2 c)))) |
| 2 | 1 | lan 77 |
. . 3
(((a →2 b) ∩ ((b
∪ c)⊥ ∪ ((a →2 b) ∩ (a
→2 c)))) ∩ ((a →2 b) ∩ ((b
∪ c)⊥ ∪ ((a →2 b) ∩ (a
→2 c))))) = (((a →2 b) ∩ ((b
∪ c)⊥ ∪ ((a →2 b) ∩ (a
→2 c)))) ∩ ((a →2 c) ∩ ((b
∪ c)⊥ ∪ ((a →2 b) ∩ (a
→2 c))))) |
| 3 | | anidm 111 |
. . . 4
(((a →2 b) ∩ ((b
∪ c)⊥ ∪ ((a →2 b) ∩ (a
→2 c)))) ∩ ((a →2 b) ∩ ((b
∪ c)⊥ ∪ ((a →2 b) ∩ (a
→2 c))))) = ((a →2 b) ∩ ((b
∪ c)⊥ ∪ ((a →2 b) ∩ (a
→2 c)))) |
| 4 | 3 | ax-r1 35 |
. . 3
((a →2 b) ∩ ((b
∪ c)⊥ ∪ ((a →2 b) ∩ (a
→2 c)))) = (((a →2 b) ∩ ((b
∪ c)⊥ ∪ ((a →2 b) ∩ (a
→2 c)))) ∩ ((a →2 b) ∩ ((b
∪ c)⊥ ∪ ((a →2 b) ∩ (a
→2 c))))) |
| 5 | | anandir 115 |
. . 3
(((a →2 b) ∩ (a
→2 c)) ∩ ((b ∪ c)⊥ ∪ ((a →2 b) ∩ (a
→2 c)))) = (((a →2 b) ∩ ((b
∪ c)⊥ ∪ ((a →2 b) ∩ (a
→2 c)))) ∩ ((a →2 c) ∩ ((b
∪ c)⊥ ∪ ((a →2 b) ∩ (a
→2 c))))) |
| 6 | 2, 4, 5 | 3tr1 63 |
. 2
((a →2 b) ∩ ((b
∪ c)⊥ ∪ ((a →2 b) ∩ (a
→2 c)))) = (((a →2 b) ∩ (a
→2 c)) ∩ ((b ∪ c)⊥ ∪ ((a →2 b) ∩ (a
→2 c)))) |
| 7 | | ax-a2 31 |
. . 3
((b ∪ c)⊥ ∪ ((a →2 b) ∩ (a
→2 c))) = (((a →2 b) ∩ (a
→2 c)) ∪ (b ∪ c)⊥ ) |
| 8 | 7 | lan 77 |
. 2
(((a →2 b) ∩ (a
→2 c)) ∩ ((b ∪ c)⊥ ∪ ((a →2 b) ∩ (a
→2 c)))) = (((a →2 b) ∩ (a
→2 c)) ∩ (((a →2 b) ∩ (a
→2 c)) ∪ (b ∪ c)⊥ )) |
| 9 | | anabs 121 |
. 2
(((a →2 b) ∩ (a
→2 c)) ∩ (((a →2 b) ∩ (a
→2 c)) ∪ (b ∪ c)⊥ )) = ((a →2 b) ∩ (a
→2 c)) |
| 10 | 6, 8, 9 | 3tr 65 |
1
((a →2 b) ∩ ((b
∪ c)⊥ ∪ ((a →2 b) ∩ (a
→2 c)))) = ((a →2 b) ∩ (a
→2 c)) |
