Metamath Proof Explorer


Theorem bibif

Description: Transfer negation via an equivalence. (Contributed by NM, 3-Oct-2007) (Proof shortened by Wolf Lammen, 28-Jan-2013)

Ref Expression
Assertion bibif ( ¬ 𝜓 → ( ( 𝜑𝜓 ) ↔ ¬ 𝜑 ) )

Proof

Step Hyp Ref Expression
1 nbn2 ( ¬ 𝜓 → ( ¬ 𝜑 ↔ ( 𝜓𝜑 ) ) )
2 bicom ( ( 𝜓𝜑 ) ↔ ( 𝜑𝜓 ) )
3 1 2 bitr2di ( ¬ 𝜓 → ( ( 𝜑𝜓 ) ↔ ¬ 𝜑 ) )