Metamath Proof Explorer


Theorem nanbi1

Description: Introduce a right anti-conjunct to both sides of a logical equivalence. (Contributed by Anthony Hart, 1-Sep-2011) (Proof shortened by Wolf Lammen, 27-Jun-2020)

Ref Expression
Assertion nanbi1 φ ψ φ χ ψ χ

Proof

Step Hyp Ref Expression
1 imbi1 φ ψ φ ¬ χ ψ ¬ χ
2 dfnan2 φ χ φ ¬ χ
3 dfnan2 ψ χ ψ ¬ χ
4 1 2 3 3bitr4g φ ψ φ χ ψ χ