Theorem df3or2

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

	Ref	Expression
Assertion	df3or2	$$⊢\left(\phi \vee \psi \vee \chi \right)\leftrightarrow \left(\neg \phi \to \left(\neg \psi \to \chi \right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		df-3or	$$⊢\left(\phi \vee \psi \vee \chi \right)\leftrightarrow \left(\left(\phi \vee \psi \right)\vee \chi \right)$$
2		df-or	$$⊢\left(\left(\phi \vee \psi \right)\vee \chi \right)\leftrightarrow \left(\neg \left(\phi \vee \psi \right)\to \chi \right)$$
3		ioran	$$⊢\neg \left(\phi \vee \psi \right)\leftrightarrow \left(\neg \phi \wedge \neg \psi \right)$$
4	3	imbi1i	$$⊢\left(\neg \left(\phi \vee \psi \right)\to \chi \right)\leftrightarrow \left(\left(\neg \phi \wedge \neg \psi \right)\to \chi \right)$$
5		impexp	$$⊢\left(\left(\neg \phi \wedge \neg \psi \right)\to \chi \right)\leftrightarrow \left(\neg \phi \to \left(\neg \psi \to \chi \right)\right)$$
6	4 5	bitri	$$⊢\left(\neg \left(\phi \vee \psi \right)\to \chi \right)\leftrightarrow \left(\neg \phi \to \left(\neg \psi \to \chi \right)\right)$$
7	2 6	bitri	$$⊢\left(\left(\phi \vee \psi \right)\vee \chi \right)\leftrightarrow \left(\neg \phi \to \left(\neg \psi \to \chi \right)\right)$$
8	1 7	bitri	$$⊢\left(\phi \vee \psi \vee \chi \right)\leftrightarrow \left(\neg \phi \to \left(\neg \psi \to \chi \right)\right)$$