Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-nor Structured version   Visualization version   GIF version

Definition df-nor 1522
 Description: Define joint denial ("not-or" or "nor"). After we define the constant true ⊤ (df-tru 1541) and the constant false ⊥ (df-fal 1551), we will be able to prove these truth table values: ((⊤ ⊽ ⊤) ↔ ⊥) (trunortru 1587), ((⊤ ⊽ ⊥) ↔ ⊥) (trunorfal 1589), ((⊥ ⊽ ⊤) ↔ ⊥) (falnortru 1591), and ((⊥ ⊽ ⊥) ↔ ⊤) (falnorfal 1592). Contrast with ∧ (df-an 400), ∨ (df-or 845), → (wi 4), ⊼ (df-nan 1483), and ⊻ (df-xor 1503). (Contributed by Remi, 25-Oct-2023.)
Assertion
Ref Expression
df-nor ((𝜑 𝜓) ↔ ¬ (𝜑𝜓))

Detailed syntax breakdown of Definition df-nor
StepHypRef Expression
1 wph . . 3 wff 𝜑
2 wps . . 3 wff 𝜓
31, 2wnor 1521 . 2 wff (𝜑 𝜓)
41, 2wo 844 . . 3 wff (𝜑𝜓)
54wn 3 . 2 wff ¬ (𝜑𝜓)
63, 5wb 209 1 wff ((𝜑 𝜓) ↔ ¬ (𝜑𝜓))
 Colors of variables: wff setvar class This definition is referenced by:  norcom  1523  norcomOLD  1524  nornot  1525  nornotOLD  1526  noran  1527  noranOLD  1528  noror  1529  nororOLD  1530  norasslem1  1531  norass  1534  norassOLD  1535  trunortru  1587  trunortruOLD  1588  trunorfal  1589  trunorfalOLD  1590  falnorfal  1592  falnorfalOLD  1593  wl-df3maxtru1  34976
 Copyright terms: Public domain W3C validator