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- ( 𝜑 , ¬ 𝜓 , 𝜓 ) ↔ ( 𝜑 ⊻ 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		ifpdfbi	⊢ ( ( ¬ 𝜑 ↔ 𝜓 ) ↔ if- ( ¬ 𝜑 , 𝜓 , ¬ 𝜓 ) )
2		df-xor	⊢ ( ( 𝜑 ⊻ 𝜓 ) ↔ ¬ ( 𝜑 ↔ 𝜓 ) )
3		nbbn	⊢ ( ( ¬ 𝜑 ↔ 𝜓 ) ↔ ¬ ( 𝜑 ↔ 𝜓 ) )
4	2 3	bitr4i	⊢ ( ( 𝜑 ⊻ 𝜓 ) ↔ ( ¬ 𝜑 ↔ 𝜓 ) )
5		ifpn	⊢ ( if- ( 𝜑 , ¬ 𝜓 , 𝜓 ) ↔ if- ( ¬ 𝜑 , 𝜓 , ¬ 𝜓 ) )
6	1 4 5	3bitr4ri	⊢ ( if- ( 𝜑 , ¬ 𝜓 , 𝜓 ) ↔ ( 𝜑 ⊻ 𝜓 ) )