ifpdfxor

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

		Ref	Expression
	Assertion	ifpdfxor	$⊢ (φ ⊻ ψ) \leftrightarrow if- (φ, \neg ψ, ψ)$

Step	Hyp	Ref	Expression
1		xor2	$⊢ (φ ⊻ ψ) \leftrightarrow ((φ \lor ψ) \land \neg (φ \land ψ))$
2		ifpdfor	$⊢ (φ \lor ψ) \leftrightarrow if- (φ, ⊤, ψ)$
3		ifpnot23	$⊢ \neg if- (φ, ψ, ⊥) \leftrightarrow if- (φ, \neg ψ, \neg ⊥)$
4		ifpdfan	$⊢ (φ \land ψ) \leftrightarrow if- (φ, ψ, ⊥)$
5	3 4	xchnxbir	$⊢ \neg (φ \land ψ) \leftrightarrow if- (φ, \neg ψ, \neg ⊥)$
6	2 5	anbi12i	$⊢ ((φ \lor ψ) \land \neg (φ \land ψ)) \leftrightarrow (if- (φ, ⊤, ψ) \land if- (φ, \neg ψ, \neg ⊥))$
7		ifpan23	$⊢ (if- (φ, ⊤, ψ) \land if- (φ, \neg ψ, \neg ⊥)) \leftrightarrow if- (φ, (⊤ \land \neg ψ), (ψ \land \neg ⊥))$
8		truan	$⊢ (⊤ \land \neg ψ) \leftrightarrow \neg ψ$
9		fal	$⊢ \neg ⊥$
10	9	biantru	$⊢ ψ \leftrightarrow (ψ \land \neg ⊥)$
11	10	bicomi	$⊢ (ψ \land \neg ⊥) \leftrightarrow ψ$
12		ifpbi23	$⊢ (((⊤ \land \neg ψ) \leftrightarrow \neg ψ) \land ((ψ \land \neg ⊥) \leftrightarrow ψ)) \to (if- (φ, (⊤ \land \neg ψ), (ψ \land \neg ⊥)) \leftrightarrow if- (φ, \neg ψ, ψ))$
13	8 11 12	mp2an	$⊢ if- (φ, (⊤ \land \neg ψ), (ψ \land \neg ⊥)) \leftrightarrow if- (φ, \neg ψ, ψ)$
14	7 13	bitri	$⊢ (if- (φ, ⊤, ψ) \land if- (φ, \neg ψ, \neg ⊥)) \leftrightarrow if- (φ, \neg ψ, ψ)$
15	1 6 14	3bitri	$⊢ (φ ⊻ ψ) \leftrightarrow if- (φ, \neg ψ, ψ)$

Metamath Proof Explorer