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 ( 𝜓 ↔ ( 𝜑𝜓 ) )