Metamath Proof Explorer


Theorem bj-andnotim

Description: Two ways of expressing a certain ternary connective. Note the respective positions of the three formulas on each side of the biconditional. (Contributed by BJ, 6-Oct-2018)

Ref Expression
Assertion bj-andnotim φ ¬ ψ χ φ ψ χ

Proof

Step Hyp Ref Expression
1 imor φ ¬ ψ χ ¬ φ ¬ ψ χ
2 iman φ ψ ¬ φ ¬ ψ
3 2 biimpri ¬ φ ¬ ψ φ ψ
4 3 orim1i ¬ φ ¬ ψ χ φ ψ χ
5 1 4 sylbi φ ¬ ψ χ φ ψ χ
6 pm2.24 ψ ¬ ψ χ
7 6 imim2i φ ψ φ ¬ ψ χ
8 7 impd φ ψ φ ¬ ψ χ
9 ax-1 χ φ ¬ ψ χ
10 8 9 jaoi φ ψ χ φ ¬ ψ χ
11 5 10 impbii φ ¬ ψ χ φ ψ χ