Metamath Proof Explorer

Theorem bj-imn3ani

Description: Duplication of bnj1224 . Three-fold version of imnani . (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (Revised by BJ, 22-Oct-2019) (Proof modification is discouraged.)

Ref Expression
Hypothesis bj-imn3ani.1 ¬ φ ψ χ
Assertion bj-imn3ani φ ψ ¬ χ


Step Hyp Ref Expression
1 bj-imn3ani.1 ¬ φ ψ χ
2 df-3an φ ψ χ φ ψ χ
3 1 2 mtbi ¬ φ ψ χ
4 3 imnani φ ψ ¬ χ