Metamath Proof Explorer


Theorem nbbnOLD

Description: Obsolete version of nbbn as of 10-Jun-2026. (Contributed by NM, 27-Jun-2002) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion nbbnOLD ¬ φ ψ ¬ φ ψ

Proof

Step Hyp Ref Expression
1 xor3 ¬ φ ψ φ ¬ ψ
2 con2bi φ ¬ ψ ψ ¬ φ
3 bicom ψ ¬ φ ¬ φ ψ
4 1 2 3 3bitrri ¬ φ ψ ¬ φ ψ