Definition df-nor 1523

Description: Define joint denial ("not-or" or "nor"). After we define the constant true ⊤ (df-tru 1542) and the constant false ⊥ (df-fal 1552), we will be able to prove these truth table values: ((⊤ ⊽ ⊤) ↔ ⊥) (trunortru 1588), ((⊤ ⊽ ⊥) ↔ ⊥) (trunorfal 1590), ((⊥ ⊽ ⊤) ↔ ⊥) (falnortru 1592), and ((⊥ ⊽ ⊥) ↔ ⊤) (falnorfal 1593). Contrast with ∧ (df-an 396), ∨ (df-or 844), → (wi 4), ⊼ (df-nan 1484), and ⊻ (df-xor 1504). (Contributed by Remi, 25-Oct-2023.)

Assertion

Ref	Expression
df-nor	⊢ ((𝜑 ⊽ 𝜓) ↔ ¬ (𝜑 ∨ 𝜓))

Detailed syntax breakdown of Definition df-nor

Step	Hyp	Ref	Expression
1		wph	. . 3 wff 𝜑
2		wps	. . 3 wff 𝜓
3	1, 2	wnor 1522	. 2 wff (𝜑 ⊽ 𝜓)
4	1, 2	wo 843	. . 3 wff (𝜑 ∨ 𝜓)
5	4	wn 3	. 2 wff ¬ (𝜑 ∨ 𝜓)
6	3, 5	wb 205	1 wff ((𝜑 ⊽ 𝜓) ↔ ¬ (𝜑 ∨ 𝜓))

This definition is referenced by:  norcom  1524  norcomOLD  1525  nornot  1526  nornotOLD  1527  noran  1528  noranOLD  1529  noror  1530  nororOLD  1531  norasslem1  1532  norass  1535  norassOLD  1536  trunortru  1588  trunortruOLD  1589  trunorfal  1590  trunorfalOLD  1591  falnorfal  1593  falnorfalOLD  1594  wl-df3maxtru1  35596