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 ) ) |