Theorem wl-1xor

Description: In the recursive scheme

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

we set n = 0 to formally arrive at an expression for "1-xor". The base case "0-xor" is replaced with F. , as a sequence of 0 inputs never has an odd number being part of it. (Contributed by Wolf Lammen, 11-May-2024)

	Ref	Expression
Assertion	wl-1xor	⊢ ( if- ( 𝜓 , ¬ ⊥ , ⊥ ) ↔ 𝜓 )

Proof

Step	Hyp	Ref	Expression
1		tbtru	⊢ ( 𝜓 ↔ ( 𝜓 ↔ ⊤ ) )
2	1	biimpi	⊢ ( 𝜓 → ( 𝜓 ↔ ⊤ ) )
3		notfal	⊢ ( ¬ ⊥ ↔ ⊤ )
4	2 3	bitr4di	⊢ ( 𝜓 → ( 𝜓 ↔ ¬ ⊥ ) )
5		nbfal	⊢ ( ¬ 𝜓 ↔ ( 𝜓 ↔ ⊥ ) )
6	5	biimpi	⊢ ( ¬ 𝜓 → ( 𝜓 ↔ ⊥ ) )
7	4 6	casesifp	⊢ ( 𝜓 ↔ if- ( 𝜓 , ¬ ⊥ , ⊥ ) )
8	7	bicomi	⊢ ( if- ( 𝜓 , ¬ ⊥ , ⊥ ) ↔ 𝜓 )