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- ( ph , -. ps , ps ) <-> ( ph \/_ ps ) )

Proof

Step	Hyp	Ref	Expression
1		ifpdfbi	|- ( ( -. ph <-> ps ) <-> if- ( -. ph , ps , -. ps ) )
2		df-xor	|- ( ( ph \/_ ps ) <-> -. ( ph <-> ps ) )
3		nbbn	|- ( ( -. ph <-> ps ) <-> -. ( ph <-> ps ) )
4	2 3	bitr4i	|- ( ( ph \/_ ps ) <-> ( -. ph <-> ps ) )
5		ifpn	|- ( if- ( ph , -. ps , ps ) <-> if- ( -. ph , ps , -. ps ) )
6	1 4 5	3bitr4ri	|- ( if- ( ph , -. ps , ps ) <-> ( ph \/_ ps ) )