Description: This tautology shows that xor is really exclusive. (Contributed by FL, 22-Nov-2010)
Ref | Expression | ||
---|---|---|---|
Assertion | excxor | |- ( ( ph \/_ ps ) <-> ( ( ph /\ -. ps ) \/ ( -. ph /\ ps ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-xor | |- ( ( ph \/_ ps ) <-> -. ( ph <-> ps ) ) |
|
2 | xor | |- ( -. ( ph <-> ps ) <-> ( ( ph /\ -. ps ) \/ ( ps /\ -. ph ) ) ) |
|
3 | ancom | |- ( ( ps /\ -. ph ) <-> ( -. ph /\ ps ) ) |
|
4 | 3 | orbi2i | |- ( ( ( ph /\ -. ps ) \/ ( ps /\ -. ph ) ) <-> ( ( ph /\ -. ps ) \/ ( -. ph /\ ps ) ) ) |
5 | 1 2 4 | 3bitri | |- ( ( ph \/_ ps ) <-> ( ( ph /\ -. ps ) \/ ( -. ph /\ ps ) ) ) |