Theorem nororOLD

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

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

Proof

Step	Hyp	Ref	Expression
1		notnotb	|- ( ( ph \/ ps ) <-> -. -. ( ph \/ ps ) )
2		df-nor	|- ( ( ph -\/ ps ) <-> -. ( ph \/ ps ) )
3	2	notbii	|- ( -. ( ph -\/ ps ) <-> -. -. ( ph \/ ps ) )
4		nornot	|- ( -. ( ph -\/ ps ) <-> ( ( ph -\/ ps ) -\/ ( ph -\/ ps ) ) )
5	1 3 4	3bitr2ri	|- ( ( ( ph -\/ ps ) -\/ ( ph -\/ ps ) ) <-> ( ph \/ ps ) )
6	5	bicomi	|- ( ( ph \/ ps ) <-> ( ( ph -\/ ps ) -\/ ( ph -\/ ps ) ) )