Metamath Proof Explorer


Theorem annotanannot

Description: A conjunction with a negated conjunction. (Contributed by AV, 8-Mar-2022) (Proof shortened by Wolf Lammen, 1-Apr-2022)

Ref Expression
Assertion annotanannot φ ¬ φ ψ φ ¬ ψ

Proof

Step Hyp Ref Expression
1 ibar φ ψ φ ψ
2 1 bicomd φ φ ψ ψ
3 2 notbid φ ¬ φ ψ ¬ ψ
4 3 pm5.32i φ ¬ φ ψ φ ¬ ψ