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	⊢ ( ( 𝜑 ⊽ 𝜓 ) ↔ ¬ ( 𝜑 ∨ 𝜓 ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		wph	⊢ 𝜑
1		wps	⊢ 𝜓
2	0 1	wnor	⊢ ( 𝜑 ⊽ 𝜓 )
3	0 1	wo	⊢ ( 𝜑 ∨ 𝜓 )
4	3	wn	⊢ ¬ ( 𝜑 ∨ 𝜓 )
5	2 4	wb	⊢ ( ( 𝜑 ⊽ 𝜓 ) ↔ ¬ ( 𝜑 ∨ 𝜓 ) )