Theorem wl-2xor

Description: In the recursive scheme

"(n+1)-xor" <-> if- ( ph , -. "n-xor" , "n-xor" )

we set n = 1 to formally arrive at an expression for "2-xor". It is based on "1-xor", that is known to be equivalent to its only input (see wl-1xor ). (Contributed by Wolf Lammen, 11-May-2024)

	Ref	Expression
Assertion	wl-2xor	$$⊢if-\left(\phi ,\neg \psi ,\psi \right)\leftrightarrow \left(\phi ⊻\psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		ifpdfbi	$$⊢\left(\neg \phi \leftrightarrow \psi \right)\leftrightarrow if-\left(\neg \phi ,\psi ,\neg \psi \right)$$
2		df-xor	$$⊢\left(\phi ⊻\psi \right)\leftrightarrow \neg \left(\phi \leftrightarrow \psi \right)$$
3		nbbn	$$⊢\left(\neg \phi \leftrightarrow \psi \right)\leftrightarrow \neg \left(\phi \leftrightarrow \psi \right)$$
4	2 3	bitr4i	$$⊢\left(\phi ⊻\psi \right)\leftrightarrow \left(\neg \phi \leftrightarrow \psi \right)$$
5		ifpn	$$⊢if-\left(\phi ,\neg \psi ,\psi \right)\leftrightarrow if-\left(\neg \phi ,\psi ,\neg \psi \right)$$
6	1 4 5	3bitr4ri	$$⊢if-\left(\phi ,\neg \psi ,\psi \right)\leftrightarrow \left(\phi ⊻\psi \right)$$