Metamath Proof Explorer

Theorem nimnbi

Description: If an implication is false, the biconditional is false. (Contributed by Glauco Siliprandi, 15-Feb-2025)

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

Proof

Step Hyp Ref Expression
1 nimnbi.1 
 |-  -. ( ph -> ps )
2 biimp 
 |-  ( ( ph <-> ps ) -> ( ph -> ps ) )
3 1 2 mto 
 |-  -. ( ph <-> ps )