Metamath Proof Explorer


Theorem nanim

Description: Implication in terms of alternative denial. (Contributed by Jeff Hoffman, 19-Nov-2007)

Ref Expression
Assertion nanim φ ψ φ ψ ψ

Proof

Step Hyp Ref Expression
1 nannan φ ψ ψ φ ψ ψ
2 anidmdbi φ ψ ψ φ ψ
3 1 2 bitr2i φ ψ φ ψ ψ