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 866
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 27605). After we define the constant true (df-tru 1641) and the constant false (df-fal 1651), we will be able to prove these truth table values: ((⊤ ∨ ⊤) ↔ ⊤) (truortru 1675), ((⊤ ∨ ⊥) ↔ ⊤) (truorfal 1676), ((⊥ ∨ ⊤) ↔ ⊤) (falortru 1677), and ((⊥ ∨ ⊥) ↔ ⊥) (falorfal 1678).

Contrast with (df-an 385), (wi 4), (df-nan 1602), and (df-xor 1619). (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 865 . 2 wff (𝜑𝜓)
41wn 3 . . 3 wff ¬ 𝜑
54, 2wi 4 . 2 wff 𝜑𝜓)
63, 5wb 197 1 wff ((𝜑𝜓) ↔ (¬ 𝜑𝜓))
Colors of variables: wff setvar class
This definition is referenced by:  pm4.64  867  pm2.53  869  pm2.54  870  imor  871  ori  879  orri  880  ord  882  mtord  895  orbi2d  930  orimdi  945  orbidi  966  pm5.6  1015  ordi  1019  pm5.17  1026  nanbi  1608  cador  1702  nf4  1867  19.43  1972  nfor  1996  19.32v  2032  19.32  2269  nforOLD  2418  dfsb3  2533  sbor  2557  neor  3069  r19.30  3270  r19.32v  3271  r19.43  3281  dfif2  4281  disjor  4826  soxp  7520  unxpwdom2  8728  cflim2  9366  cfpwsdom  9687  ltapr  10148  ltxrlt  10389  isprm4  15611  euclemma  15638  islpi  21163  restntr  21196  alexsubALTlem2  22061  alexsubALTlem3  22062  2bornot2b  27647  disjorf  29713  funcnv5mpt  29792  ballotlemodife  30880  3orit  31913  dfon2lem5  32007  ecase13d  32623  elicc3  32627  nn0prpw  32634  onsucuni3  33526  orfa  34187  unitresl  34190  cnf1dd  34198  tsim1  34242  ineleq  34427  ifpidg  38330  ifpim123g  38339  ifpororb  38344  ifpor123g  38347  dfxor4  38552  df3or2  38554  frege83  38734  dffrege99  38750  frege131  38782  frege133  38784  pm10.541  39060  xrssre  40038  elprn2  40340  iundjiun  41150  r19.32  41674
  Copyright terms: Public domain W3C validator