Metamath Proof Explorer


Theorem nannan

Description: Nested alternative denials. (Contributed by Jeff Hoffman, 19-Nov-2007) (Proof shortened by Wolf Lammen, 26-Jun-2020)

Ref Expression
Assertion nannan φ ψ χ φ ψ χ

Proof

Step Hyp Ref Expression
1 dfnan2 φ ψ χ φ ¬ ψ χ
2 nanan ψ χ ¬ ψ χ
3 2 imbi2i φ ψ χ φ ¬ ψ χ
4 1 3 bitr4i φ ψ χ φ ψ χ