Description: Two ways to express "exclusive or". (Contributed by NM, 3-Jan-2005) (Proof shortened by Wolf Lammen, 24-Jan-2013)
Ref | Expression | ||
---|---|---|---|
Assertion | nbi2 | |- ( -. ( ph <-> ps ) <-> ( ( ph \/ ps ) /\ -. ( ph /\ ps ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | xor3 | |- ( -. ( ph <-> ps ) <-> ( ph <-> -. ps ) ) |
|
2 | pm5.17 | |- ( ( ( ph \/ ps ) /\ -. ( ph /\ ps ) ) <-> ( ph <-> -. ps ) ) |
|
3 | 1 2 | bitr4i | |- ( -. ( ph <-> ps ) <-> ( ( ph \/ ps ) /\ -. ( ph /\ ps ) ) ) |