Metamath Proof Explorer

Theorem abciffcbatnabciffncbai

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

		Ref	Expression
	Hypothesis	abciffcbatnabciffncbai.1	$⊢ ((φ \land ψ) \land χ) \leftrightarrow ((χ \land ψ) \land φ)$
	Assertion	abciffcbatnabciffncbai	$⊢ \neg ((φ \land ψ) \land χ) \to \neg ((χ \land ψ) \land φ)$

Proof

Step	Hyp	Ref	Expression
1		abciffcbatnabciffncbai.1	$⊢ ((φ \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 φ)$