Metamath Proof Explorer


Theorem bj-falor

Description: Dual of truan (which has biconditional reversed). (Contributed by BJ, 26-Oct-2019) (Proof modification is discouraged.)

Ref Expression
Assertion bj-falor φ φ

Proof

Step Hyp Ref Expression
1 fal ¬
2 1 bj-biorfi φ φ