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 ¬ ψ φ ψ ¬ φ