Theorem nanorxor

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

	Ref	Expression
Assertion	nanorxor	|- ( ( ph -/\ ps ) <-> ( ( ph \/ ps ) <-> ( ph \/_ ps ) ) )

Proof

Step	Hyp	Ref	Expression
1		df-nan	|- ( ( ph -/\ ps ) <-> -. ( ph /\ ps ) )
2		xor2	|- ( ( ph \/_ ps ) <-> ( ( ph \/ ps ) /\ -. ( ph /\ ps ) ) )
3	2	rbaibr	|- ( -. ( ph /\ ps ) -> ( ( ph \/ ps ) <-> ( ph \/_ ps ) ) )
4	2	bibi2i	|- ( ( ( ph \/ ps ) <-> ( ph \/_ ps ) ) <-> ( ( ph \/ ps ) <-> ( ( ph \/ ps ) /\ -. ( ph /\ ps ) ) ) )
5		pm4.71	|- ( ( ( ph \/ ps ) -> -. ( ph /\ ps ) ) <-> ( ( ph \/ ps ) <-> ( ( ph \/ ps ) /\ -. ( ph /\ ps ) ) ) )
6		simpl	|- ( ( ph /\ ps ) -> ph )
7	6	orcd	|- ( ( ph /\ ps ) -> ( ph \/ ps ) )
8	7	con3i	|- ( -. ( ph \/ ps ) -> -. ( ph /\ ps ) )
9		id	|- ( -. ( ph /\ ps ) -> -. ( ph /\ ps ) )
10	8 9	ja	|- ( ( ( ph \/ ps ) -> -. ( ph /\ ps ) ) -> -. ( ph /\ ps ) )
11	5 10	sylbir	|- ( ( ( ph \/ ps ) <-> ( ( ph \/ ps ) /\ -. ( ph /\ ps ) ) ) -> -. ( ph /\ ps ) )
12	4 11	sylbi	|- ( ( ( ph \/ ps ) <-> ( ph \/_ ps ) ) -> -. ( ph /\ ps ) )
13	3 12	impbii	|- ( -. ( ph /\ ps ) <-> ( ( ph \/ ps ) <-> ( ph \/_ ps ) ) )
14	1 13	bitri	|- ( ( ph -/\ ps ) <-> ( ( ph \/ ps ) <-> ( ph \/_ ps ) ) )