Definition df-nor

Description: Define joint denial ("not-or" or "nor"). After we define the constant true T. ( df-tru ) and the constant false F. ( df-fal ), we will be able to prove these truth table values: ( ( T. -\/ T. ) <-> F. ) ( trunortru ), ( ( T. -\/ F. ) <-> F. ) ( trunorfal ), ( ( F. -\/ T. ) <-> F. ) ( falnortru ), and ( ( F. -\/ F. ) <-> T. ) ( falnorfal ). Contrast with /\ ( df-an ), \/ ( df-or ), -> ( wi ), -/\ ( df-nan ), and \/_ ( df-xor ). (Contributed by Remi, 25-Oct-2023)

	Ref	Expression
Assertion	df-nor	|- ( ( ph -\/ ps ) <-> -. ( ph \/ ps ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		wph	|- ph
1		wps	|- ps
2	0 1	wnor	|- ( ph -\/ ps )
3	0 1	wo	|- ( ph \/ ps )
4	3	wn	|- -. ( ph \/ ps )
5	2 4	wb	|- ( ( ph -\/ ps ) <-> -. ( ph \/ ps ) )