Description: Obsolete version of norcom as of 23-Apr-2024. (Contributed by Remi, 25-Oct-2023) (Proof modification is discouraged.) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | norcomOLD | |- ( ( ph -\/ ps ) <-> ( ps -\/ ph ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | orcom | |- ( ( ph \/ ps ) <-> ( ps \/ ph ) ) |
|
| 2 | 1 | notbii | |- ( -. ( ph \/ ps ) <-> -. ( ps \/ ph ) ) |
| 3 | df-nor | |- ( ( ph -\/ ps ) <-> -. ( ph \/ ps ) ) |
|
| 4 | df-nor | |- ( ( ps -\/ ph ) <-> -. ( ps \/ ph ) ) |
|
| 5 | 2 3 4 | 3bitr4i | |- ( ( ph -\/ ps ) <-> ( ps -\/ ph ) ) |