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	$$⊢\left(\phi ⊽\psi \right)\leftrightarrow \neg \left(\phi \vee \psi \right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		wph	$$wff\phi$$
1		wps	$$wff\psi$$
2	0 1	wnor	$$wff\left(\phi ⊽\psi \right)$$
3	0 1	wo	$$wff\left(\phi \vee \psi \right)$$
4	3	wn	$$wff\neg \left(\phi \vee \psi \right)$$
5	2 4	wb	$$wff\left(\left(\phi ⊽\psi \right)\leftrightarrow \neg \left(\phi \vee \psi \right)\right)$$