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 845
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 28204). 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: ((⊤ ∨ ⊤) ↔ ⊤) (truortru 1575), ((⊤ ∨ ⊥) ↔ ⊤) (truorfal 1576), ((⊥ ∨ ⊤) ↔ ⊤) (falortru 1577), and ((⊥ ∨ ⊥) ↔ ⊥) (falorfal 1578).

Contrast with (df-an 400), (wi 4), (df-nan 1483), and (df-xor 1503). (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 844 . 2 wff (𝜑𝜓)
41wn 3 . . 3 wff ¬ 𝜑
54, 2wi 4 . 2 wff 𝜑𝜓)
63, 5wb 209 1 wff ((𝜑𝜓) ↔ (¬ 𝜑𝜓))
Colors of variables: wff setvar class
This definition is referenced by:  pm4.64  846  pm2.53  848  pm2.54  849  imor  850  ori  858  orri  859  ord  861  unitreslOLD  875  orbi2d  913  orimdi  928  orbidi  950  pm5.6  999  ordi  1003  pm5.17  1009  nanbi  1491  cador  1610  nf4  1789  19.43  1883  nfor  1905  19.32v  1941  19.32  2236  sbor  2317  dfsb3  2533  dfsb3ALT  2592  neor  3102  r19.32v  3322  r19.43  3332  dfif2  4441  disjor  5022  soxp  7810  unxpwdom2  9040  cflim2  9674  cfpwsdom  9995  ltapr  10456  ltxrlt  10700  isprm4  16017  euclemma  16046  islpi  21752  restntr  21785  alexsubALTlem2  22651  alexsubALTlem3  22652  2bornot2b  28247  disjorf  30337  funcnv5mpt  30421  dvdszzq  30541  cycpm2tr  30792  ballotlemodife  31829  3orit  33019  dfon2lem5  33106  ecase13d  33735  elicc3  33739  nn0prpw  33745  onsucuni3  34745  orfa  35478  cnf1dd  35486  tsim1  35526  ineleq  35726  ifpidg  40129  ifpim123g  40138  ifpororb  40143  ifpor123g  40146  dfxor4  40397  df3or2  40399  frege83  40578  dffrege99  40594  frege131  40626  frege133  40628  pm10.541  41005  xrssre  41919  elprn2  42215  iundjiun  43038  r19.32  43592
  Copyright terms: Public domain W3C validator