Theorem noranOLD

Description: Obsolete version of noran as of 8-Dec-2023. (Contributed by Remi, 26-Oct-2023) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		ianor	|- ( -. ( ph /\ ps ) <-> ( -. ph \/ -. ps ) )
2	1	notbii	|- ( -. -. ( ph /\ ps ) <-> -. ( -. ph \/ -. ps ) )
3		nornot	|- ( -. ph <-> ( ph -\/ ph ) )
4		nornot	|- ( -. ps <-> ( ps -\/ ps ) )
5	3 4	orbi12i	|- ( ( -. ph \/ -. ps ) <-> ( ( ph -\/ ph ) \/ ( ps -\/ ps ) ) )
6	5	notbii	|- ( -. ( -. ph \/ -. ps ) <-> -. ( ( ph -\/ ph ) \/ ( ps -\/ ps ) ) )
7		ioran	|- ( -. ( ( ph -\/ ph ) \/ ( ps -\/ ps ) ) <-> ( -. ( ph -\/ ph ) /\ -. ( ps -\/ ps ) ) )
8	2 6 7	3bitrri	|- ( ( -. ( ph -\/ ph ) /\ -. ( ps -\/ ps ) ) <-> -. -. ( ph /\ ps ) )
9		df-nor	|- ( ( ( ph -\/ ph ) -\/ ( ps -\/ ps ) ) <-> -. ( ( ph -\/ ph ) \/ ( ps -\/ ps ) ) )
10	9 7	bitri	|- ( ( ( ph -\/ ph ) -\/ ( ps -\/ ps ) ) <-> ( -. ( ph -\/ ph ) /\ -. ( ps -\/ ps ) ) )
11		notnotb	|- ( ( ph /\ ps ) <-> -. -. ( ph /\ ps ) )
12	8 10 11	3bitr4ri	|- ( ( ph /\ ps ) <-> ( ( ph -\/ ph ) -\/ ( ps -\/ ps ) ) )