Metamath Proof Explorer


Theorem biorfi

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

Proof

Step Hyp Ref Expression
1 biorfi.1
 |-  -. ph
2 biorf
 |-  ( -. ph -> ( ps <-> ( ph \/ ps ) ) )
3 1 2 ax-mp
 |-  ( ps <-> ( ph \/ ps ) )