Description: Equivalence of two ternary operations. Note the identical order and parenthesizing of the three arguments in both expressions. (Contributed by BJ, 31-Dec-2023)
Ref | Expression | ||
---|---|---|---|
Assertion | bj-bixor | |- ( ( ph <-> ( ps \/_ ch ) ) <-> ( ph \/_ ( ps <-> ch ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pm5.18 | |- ( ( ph <-> ( ps <-> ch ) ) <-> -. ( ph <-> -. ( ps <-> ch ) ) ) |
|
2 | 1 | con2bii | |- ( ( ph <-> -. ( ps <-> ch ) ) <-> -. ( ph <-> ( ps <-> ch ) ) ) |
3 | df-xor | |- ( ( ps \/_ ch ) <-> -. ( ps <-> ch ) ) |
|
4 | 3 | bibi2i | |- ( ( ph <-> ( ps \/_ ch ) ) <-> ( ph <-> -. ( ps <-> ch ) ) ) |
5 | df-xor | |- ( ( ph \/_ ( ps <-> ch ) ) <-> -. ( ph <-> ( ps <-> ch ) ) ) |
|
6 | 2 4 5 | 3bitr4i | |- ( ( ph <-> ( ps \/_ ch ) ) <-> ( ph \/_ ( ps <-> ch ) ) ) |