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 φ¬ψχφψχ