Description: Obsolete version of xorcom as of 21-Apr-2024. (Contributed by Mario Carneiro, 4-Sep-2016) (Proof modification is discouraged.) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | xorcomOLD | |- ( ( ph \/_ ps ) <-> ( ps \/_ ph ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | bicom | |- ( ( ph <-> ps ) <-> ( ps <-> ph ) ) |
|
| 2 | 1 | notbii | |- ( -. ( ph <-> ps ) <-> -. ( ps <-> ph ) ) |
| 3 | df-xor | |- ( ( ph \/_ ps ) <-> -. ( ph <-> ps ) ) |
|
| 4 | df-xor | |- ( ( ps \/_ ph ) <-> -. ( ps <-> ph ) ) |
|
| 5 | 2 3 4 | 3bitr4i | |- ( ( ph \/_ ps ) <-> ( ps \/_ ph ) ) |