Metamath Proof Explorer

Theorem nimnbi2

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

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

Proof

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