Metamath Proof Explorer
Description: Equivalence theorem for triple xor. Copy of hadbi123i . (Contributed by Mario Carneiro, 4-Sep-2016)
|
|
Ref |
Expression |
|
Hypotheses |
wl-3xorbii.1 |
|
|
|
wl-3xorbii.2 |
|
|
|
wl-3xorbii.3 |
|
|
Assertion |
wl-3xorbi123i |
|
Proof
Step |
Hyp |
Ref |
Expression |
1 |
|
wl-3xorbii.1 |
|
2 |
|
wl-3xorbii.2 |
|
3 |
|
wl-3xorbii.3 |
|
4 |
1
|
a1i |
|
5 |
2
|
a1i |
|
6 |
3
|
a1i |
|
7 |
4 5 6
|
wl-3xorbi123d |
|
8 |
7
|
mptru |
|