Description: The disjunction of the four possible combinations of two wffs and their negations is always true. A four-way excluded middle (see exmid ). (Contributed by David Abernethy, 28-Jan-2014) (Proof shortened by NM, 29-Oct-2021)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | 4exmid | |- ( ( ( ph /\ ps ) \/ ( -. ph /\ -. ps ) ) \/ ( ( ph /\ -. ps ) \/ ( ps /\ -. ph ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | pm5.24 | |- ( -. ( ( ph /\ ps ) \/ ( -. ph /\ -. ps ) ) <-> ( ( ph /\ -. ps ) \/ ( ps /\ -. ph ) ) ) |
|
| 2 | 1 | biimpi | |- ( -. ( ( ph /\ ps ) \/ ( -. ph /\ -. ps ) ) -> ( ( ph /\ -. ps ) \/ ( ps /\ -. ph ) ) ) |
| 3 | 2 | orri | |- ( ( ( ph /\ ps ) \/ ( -. ph /\ -. ps ) ) \/ ( ( ph /\ -. ps ) \/ ( ps /\ -. ph ) ) ) |