Metamath Proof Explorer

Theorem bj-falor2

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

Ref Expression
Assertion bj-falor2 
|- ( ( F. \/ ph ) <-> ph )

Proof

Step Hyp Ref Expression
1 falim 
 |-  ( F. -> ph )
2 1 bj-jaoi1 
 |-  ( ( F. \/ ph ) -> ph )
3 olc 
 |-  ( ph -> ( F. \/ ph ) )
4 2 3 impbii 
 |-  ( ( F. \/ ph ) <-> ph )