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- ψ ¬ ψ

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- ψ ¬ ψ