Metamath Proof Explorer

Theorem abciffcbatnabciffncba

Description: Operands in a biconditional expression converted negated. Additionally biconditional converted to show antecedent implies sequent. Closed form. (Contributed by Jarvin Udandy, 7-Sep-2020)

		Ref	Expression
	Assertion	abciffcbatnabciffncba	$⊢ \neg ((φ \land ψ) \land χ) \to \neg ((χ \land ψ) \land φ)$

Proof

Step	Hyp	Ref	Expression
1		an31	$⊢ ((φ \land ψ) \land χ) \leftrightarrow ((χ \land ψ) \land φ)$
2		notbi	$⊢ (((φ \land ψ) \land χ) \leftrightarrow ((χ \land ψ) \land φ)) \leftrightarrow (\neg ((φ \land ψ) \land χ) \leftrightarrow \neg ((χ \land ψ) \land φ))$
3	2	biimpi	$⊢ (((φ \land ψ) \land χ) \leftrightarrow ((χ \land ψ) \land φ)) \to (\neg ((φ \land ψ) \land χ) \leftrightarrow \neg ((χ \land ψ) \land φ))$
4	1 3	ax-mp	$⊢ \neg ((φ \land ψ) \land χ) \leftrightarrow \neg ((χ \land ψ) \land φ)$
5	4	biimpi	$⊢ \neg ((φ \land ψ) \land χ) \to \neg ((χ \land ψ) \land φ)$