Metamath Proof Explorer

Theorem norbi

Description: If neither of two propositions is true, then these propositions are equivalent. (Contributed by BJ, 26-Apr-2019)

Ref Expression
Assertion norbi 
|- ( -. ( ph \/ ps ) -> ( ph <-> ps ) )

Proof

Step Hyp Ref Expression
1 orc 
 |-  ( ph -> ( ph \/ ps ) )
2 olc 
 |-  ( ps -> ( ph \/ ps ) )
3 1 2 pm5.21ni 
 |-  ( -. ( ph \/ ps ) -> ( ph <-> ps ) )