Metamath Proof Explorer

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- (ψ, \neg ⊥, ⊥) \leftrightarrow ψ$

Proof

Step	Hyp	Ref	Expression
1		tbtru	$⊢ ψ \leftrightarrow (ψ \leftrightarrow ⊤)$
2	1	biimpi	$⊢ ψ \to (ψ \leftrightarrow ⊤)$
3		notfal	$⊢ \neg ⊥ \leftrightarrow ⊤$
4	2 3	bitr4di	$⊢ ψ \to (ψ \leftrightarrow \neg ⊥)$
5		nbfal	$⊢ \neg ψ \leftrightarrow (ψ \leftrightarrow ⊥)$
6	5	biimpi	$⊢ \neg ψ \to (ψ \leftrightarrow ⊥)$
7	4 6	casesifp	$⊢ ψ \leftrightarrow if- (ψ, \neg ⊥, ⊥)$
8	7	bicomi	$⊢ if- (ψ, \neg ⊥, ⊥) \leftrightarrow ψ$