Metamath Proof Explorer

Theorem notbicom

Description: Commutative law for the negation of a biconditional. (Contributed by Glauco Siliprandi, 15-Feb-2025)

Ref Expression
Hypothesis notbicom.1 
|- -. ( ph <-> ps )
Assertion notbicom 
|- -. ( ps <-> ph )

Proof

Step Hyp Ref Expression
1 notbicom.1 
 |-  -. ( ph <-> ps )
2 bicom 
 |-  ( ( ps <-> ph ) <-> ( ph <-> ps ) )
3 1 2 mtbir 
 |-  -. ( ps <-> ph )