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 ¬ φ
Assertion biorfi ψ φ ψ

Proof

Step Hyp Ref Expression
1 biorfi.1 ¬ φ
2 biorf ¬ φ ψ φ ψ
3 1 2 ax-mp ψ φ ψ