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

Definition df-or 842
Description: Define disjunction (logical "or"). Definition of [Margaris] p. 49. When the left operand, right operand, or both are true, the result is true; when both sides are false, the result is false. For example, it is true that (2 = 3 ∨ 4 = 4) (ex-or 28128). After we define the constant true (df-tru 1531) and the constant false (df-fal 1541), we will be able to prove these truth table values: ((⊤ ∨ ⊤) ↔ ⊤) (truortru 1565), ((⊤ ∨ ⊥) ↔ ⊤) (truorfal 1566), ((⊥ ∨ ⊤) ↔ ⊤) (falortru 1567), and ((⊥ ∨ ⊥) ↔ ⊥) (falorfal 1568).

Contrast with (df-an 397), (wi 4), (df-nan 1476), and (df-xor 1496). (Contributed by NM, 27-Dec-1992.)

Assertion
Ref Expression
df-or ((𝜑𝜓) ↔ (¬ 𝜑𝜓))

Detailed syntax breakdown of Definition df-or
StepHypRef Expression
1 wph . . 3 wff 𝜑
2 wps . . 3 wff 𝜓
31, 2wo 841 . 2 wff (𝜑𝜓)
41wn 3 . . 3 wff ¬ 𝜑
54, 2wi 4 . 2 wff 𝜑𝜓)
63, 5wb 207 1 wff ((𝜑𝜓) ↔ (¬ 𝜑𝜓))
Colors of variables: wff setvar class
This definition is referenced by:  pm4.64  843  pm2.53  845  pm2.54  846  imor  847  ori  855  orri  856  ord  858  unitresl  866  orbi2d  909  orimdi  924  orbidi  946  pm5.6  995  ordi  999  pm5.17  1005  nanbi  1484  cador  1600  nf4  1779  19.43  1874  nfor  1896  19.32v  1932  19.32  2226  sbor  2308  dfsb3  2529  dfsb3ALT  2588  neor  3108  r19.30OLD  3339  r19.32v  3340  r19.43  3351  dfif2  4467  disjor  5038  soxp  7814  unxpwdom2  9041  cflim2  9674  cfpwsdom  9995  ltapr  10456  ltxrlt  10700  isprm4  16018  euclemma  16047  islpi  21687  restntr  21720  alexsubALTlem2  22586  alexsubALTlem3  22587  2bornot2b  28171  disjorf  30258  funcnv5mpt  30342  dvdszzq  30458  cycpm2tr  30689  ballotlemodife  31655  3orit  32843  dfon2lem5  32930  ecase13d  33559  elicc3  33563  nn0prpw  33569  onsucuni3  34531  orfa  35243  cnf1dd  35251  tsim1  35291  ineleq  35491  ifpidg  39737  ifpim123g  39746  ifpororb  39751  ifpor123g  39754  dfxor4  39991  df3or2  39993  frege83  40172  dffrege99  40188  frege131  40220  frege133  40222  pm10.541  40579  xrssre  41496  elprn2  41795  iundjiun  42623  r19.32  43177
  Copyright terms: Public domain W3C validator