Metamath Proof Explorer

Theorem df3an2

Description: Express triple-and in terms of implication and negation. Statement in Frege1879 p. 12. (Contributed by RP, 25-Jul-2020)

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

Step	Hyp	Ref	Expression
1		df-3an	$⊢ (φ \land ψ \land χ) \leftrightarrow ((φ \land ψ) \land χ)$
2		df-an	$⊢ ((φ \land ψ) \land χ) \leftrightarrow \neg ((φ \land ψ) \to \neg χ)$
3		impexp	$⊢ ((φ \land ψ) \to \neg χ) \leftrightarrow (φ \to (ψ \to \neg χ))$
4	2 3	xchbinx	$⊢ ((φ \land ψ) \land χ) \leftrightarrow \neg (φ \to (ψ \to \neg χ))$
5	1 4	bitri	$⊢ (φ \land ψ \land χ) \leftrightarrow \neg (φ \to (ψ \to \neg χ))$