Definition df-nor 1527

Description: Define joint denial ("not-or" or "nor"). After we define the constant true ⊤ (df-tru 1546) and the constant false ⊥ (df-fal 1556), we will be able to prove these truth table values: ((⊤ ⊽ ⊤) ↔ ⊥) (trunortru 1592), ((⊤ ⊽ ⊥) ↔ ⊥) (trunorfal 1594), ((⊥ ⊽ ⊤) ↔ ⊥) (falnortru 1596), and ((⊥ ⊽ ⊥) ↔ ⊤) (falnorfal 1597). Contrast with ∧ (df-an 400), ∨ (df-or 848), → (wi 4), ⊼ (df-nan 1488), and ⊻ (df-xor 1508). (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 1526	. 2 wff (𝜑 ⊽ 𝜓)
4	1, 2	wo 847	. . 3 wff (𝜑 ∨ 𝜓)
5	4	wn 3	. 2 wff ¬ (𝜑 ∨ 𝜓)
6	3, 5	wb 209	1 wff ((𝜑 ⊽ 𝜓) ↔ ¬ (𝜑 ∨ 𝜓))

This definition is referenced by:  norcom  1528  norcomOLD  1529  nornot  1530  nornotOLD  1531  noran  1532  noranOLD  1533  noror  1534  nororOLD  1535  norasslem1  1536  norass  1539  norassOLD  1540  trunortru  1592  trunortruOLD  1593  trunorfal  1594  trunorfalOLD  1595  falnorfal  1597  falnorfalOLD  1598  wl-df3maxtru1  35400