Description: Alternative definition of wl-df-3xor , using triple exclusive disjunction, or XOR3. You can add more input by appending each one with a \/_ . Copy of hadass . (Contributed by Mario Carneiro, 4-Sep-2016) df-had redefined. (Revised by Wolf Lammen, 1-May-2024)
Ref | Expression | ||
---|---|---|---|
Assertion | wl-df3xor2 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ifpn | ||
2 | wl-df-3xor | ||
3 | df-xor | ||
4 | nbbn | ||
5 | ifpdfbi | ||
6 | 3 4 5 | 3bitr2i | |
7 | 1 2 6 | 3bitr4i |