Theorem noran

Description: /\ is expressible via -\/ . (Contributed by Remi, 26-Oct-2023) (Proof shortened by Wolf Lammen, 8-Dec-2023)

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

Proof

Step	Hyp	Ref	Expression
1		anor	|- ( ( ph /\ ps ) <-> -. ( -. ph \/ -. ps ) )
2		nornot	|- ( -. ph <-> ( ph -\/ ph ) )
3		nornot	|- ( -. ps <-> ( ps -\/ ps ) )
4	2 3	orbi12i	|- ( ( -. ph \/ -. ps ) <-> ( ( ph -\/ ph ) \/ ( ps -\/ ps ) ) )
5	1 4	xchbinx	|- ( ( ph /\ ps ) <-> -. ( ( ph -\/ ph ) \/ ( ps -\/ ps ) ) )
6		df-nor	|- ( ( ( ph -\/ ph ) -\/ ( ps -\/ ps ) ) <-> -. ( ( ph -\/ ph ) \/ ( ps -\/ ps ) ) )
7	5 6	bitr4i	|- ( ( ph /\ ps ) <-> ( ( ph -\/ ph ) -\/ ( ps -\/ ps ) ) )