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 
|- ( ph <-> ( F. \/ ph ) )

Proof

Step Hyp Ref Expression
1 fal 
 |-  -. F.
2 1 bj-biorfi 
 |-  ( ph <-> ( F. \/ ph ) )