Description: The dual of biorf is not biantr but iba (and ibar ). So there should also be a "biorfr". (Note that these four statements can actually be strengthened to biconditionals.) (Contributed by BJ, 26-Oct-2019)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | biorfi.1 | |- -. ph |
|
| Assertion | biorfi | |- ( ps <-> ( ph \/ ps ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | biorfi.1 | |- -. ph |
|
| 2 | biorf | |- ( -. ph -> ( ps <-> ( ph \/ ps ) ) ) |
|
| 3 | 1 2 | ax-mp | |- ( ps <-> ( ph \/ ps ) ) |