Theorem ifpdfxor

Description: Define xor as conditional logic operator. (Contributed by RP, 20-Apr-2020)

	Ref	Expression
Assertion	ifpdfxor	⊢ ( ( 𝜑 ⊻ 𝜓 ) ↔ if- ( 𝜑 , ¬ 𝜓 , 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		xor2	⊢ ( ( 𝜑 ⊻ 𝜓 ) ↔ ( ( 𝜑 ∨ 𝜓 ) ∧ ¬ ( 𝜑 ∧ 𝜓 ) ) )
2		ifpdfor	⊢ ( ( 𝜑 ∨ 𝜓 ) ↔ if- ( 𝜑 , ⊤ , 𝜓 ) )
3		ifpnot23	⊢ ( ¬ if- ( 𝜑 , 𝜓 , ⊥ ) ↔ if- ( 𝜑 , ¬ 𝜓 , ¬ ⊥ ) )
4		ifpdfan	⊢ ( ( 𝜑 ∧ 𝜓 ) ↔ if- ( 𝜑 , 𝜓 , ⊥ ) )
5	3 4	xchnxbir	⊢ ( ¬ ( 𝜑 ∧ 𝜓 ) ↔ if- ( 𝜑 , ¬ 𝜓 , ¬ ⊥ ) )
6	2 5	anbi12i	⊢ ( ( ( 𝜑 ∨ 𝜓 ) ∧ ¬ ( 𝜑 ∧ 𝜓 ) ) ↔ ( if- ( 𝜑 , ⊤ , 𝜓 ) ∧ if- ( 𝜑 , ¬ 𝜓 , ¬ ⊥ ) ) )
7		ifpan23	⊢ ( ( if- ( 𝜑 , ⊤ , 𝜓 ) ∧ if- ( 𝜑 , ¬ 𝜓 , ¬ ⊥ ) ) ↔ if- ( 𝜑 , ( ⊤ ∧ ¬ 𝜓 ) , ( 𝜓 ∧ ¬ ⊥ ) ) )
8		truan	⊢ ( ( ⊤ ∧ ¬ 𝜓 ) ↔ ¬ 𝜓 )
9		fal	⊢ ¬ ⊥
10	9	biantru	⊢ ( 𝜓 ↔ ( 𝜓 ∧ ¬ ⊥ ) )
11	10	bicomi	⊢ ( ( 𝜓 ∧ ¬ ⊥ ) ↔ 𝜓 )
12		ifpbi23	⊢ ( ( ( ( ⊤ ∧ ¬ 𝜓 ) ↔ ¬ 𝜓 ) ∧ ( ( 𝜓 ∧ ¬ ⊥ ) ↔ 𝜓 ) ) → ( if- ( 𝜑 , ( ⊤ ∧ ¬ 𝜓 ) , ( 𝜓 ∧ ¬ ⊥ ) ) ↔ if- ( 𝜑 , ¬ 𝜓 , 𝜓 ) ) )
13	8 11 12	mp2an	⊢ ( if- ( 𝜑 , ( ⊤ ∧ ¬ 𝜓 ) , ( 𝜓 ∧ ¬ ⊥ ) ) ↔ if- ( 𝜑 , ¬ 𝜓 , 𝜓 ) )
14	7 13	bitri	⊢ ( ( if- ( 𝜑 , ⊤ , 𝜓 ) ∧ if- ( 𝜑 , ¬ 𝜓 , ¬ ⊥ ) ) ↔ if- ( 𝜑 , ¬ 𝜓 , 𝜓 ) )
15	1 6 14	3bitri	⊢ ( ( 𝜑 ⊻ 𝜓 ) ↔ if- ( 𝜑 , ¬ 𝜓 , 𝜓 ) )