nanorxor

Description: 'nand' is equivalent to the equivalence of inclusive and exclusive or. (Contributed by Steve Rodriguez, 28-Feb-2020)

		Ref	Expression
	Assertion	nanorxor	$⊢ (φ ⊼ ψ) \leftrightarrow ((φ \lor ψ) \leftrightarrow (φ ⊻ ψ))$

Step	Hyp	Ref	Expression
1		df-nan	$⊢ (φ ⊼ ψ) \leftrightarrow \neg (φ \land ψ)$
2		xor2	$⊢ (φ ⊻ ψ) \leftrightarrow ((φ \lor ψ) \land \neg (φ \land ψ))$
3	2	rbaibr	$⊢ \neg (φ \land ψ) \to ((φ \lor ψ) \leftrightarrow (φ ⊻ ψ))$
4	2	bibi2i	$⊢ ((φ \lor ψ) \leftrightarrow (φ ⊻ ψ)) \leftrightarrow ((φ \lor ψ) \leftrightarrow ((φ \lor ψ) \land \neg (φ \land ψ)))$
5		pm4.71	$⊢ ((φ \lor ψ) \to \neg (φ \land ψ)) \leftrightarrow ((φ \lor ψ) \leftrightarrow ((φ \lor ψ) \land \neg (φ \land ψ)))$
6		simpl	$⊢ (φ \land ψ) \to φ$
7	6	orcd	$⊢ (φ \land ψ) \to (φ \lor ψ)$
8	7	con3i	$⊢ \neg (φ \lor ψ) \to \neg (φ \land ψ)$
9		id	$⊢ \neg (φ \land ψ) \to \neg (φ \land ψ)$
10	8 9	ja	$⊢ ((φ \lor ψ) \to \neg (φ \land ψ)) \to \neg (φ \land ψ)$
11	5 10	sylbir	$⊢ ((φ \lor ψ) \leftrightarrow ((φ \lor ψ) \land \neg (φ \land ψ))) \to \neg (φ \land ψ)$
12	4 11	sylbi	$⊢ ((φ \lor ψ) \leftrightarrow (φ ⊻ ψ)) \to \neg (φ \land ψ)$
13	3 12	impbii	$⊢ \neg (φ \land ψ) \leftrightarrow ((φ \lor ψ) \leftrightarrow (φ ⊻ ψ))$
14	1 13	bitri	$⊢ (φ ⊼ ψ) \leftrightarrow ((φ \lor ψ) \leftrightarrow (φ ⊻ ψ))$

Metamath Proof Explorer