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

Definition df-or 361
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 21767). After we define the constant true (df-tru 1329) and the constant false (df-fal 1330), we will be able to prove these truth table values: (( ⊤ ∨ ⊤ ) ↔ ⊤ ) (truortru 1350), (( ⊤ ∨ ⊥ ) ↔ ⊤ ) (truorfal 1351), (( ⊥ ∨ ⊤ ) ↔ ⊤ ) (falortru 1352), and (( ⊥ ∨ ⊥ ) ↔ ⊥ ) (falorfal 1353).

This is our first use of the biconditional connective in a definition; we use the biconditional connective in place of the traditional "<=def=>", which means the same thing, except that we can manipulate the biconditional connective directly in proofs rather than having to rely on an informal definition substitution rule. Note that if we mechanically substitute 𝜑𝜓) for (𝜑𝜓), we end up with an instance of previously proved theorem biid 229. This is the justification for the definition, along with the fact that it introduces a new symbol . Contrast with (df-an 362), (wi 4), (df-nan 1298), and (df-xor 1315) . (Contributed by NM, 5-Aug-1993.)

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

Detailed syntax breakdown of Definition df-or
StepHypRef Expression
1 wph . . 3 wff 𝜑
2 wps . . 3 wff 𝜓
31, 2wo 359 . 2 wff (𝜑𝜓)
41wn 3 . . 3 wff ¬ 𝜑
54, 2wi 4 . 2 wff 𝜑𝜓)
63, 5wb 178 1 wff ((𝜑𝜓) ↔ (¬ 𝜑𝜓))
Colors of variables: wff set class
This definition is referenced by:  pm4.64  363  pm2.53  364  pm2.54  365  ori  366  orri  367  ord  368  imor  403  mtord  643  orbi2d  684  orimdi  822  ordi  836  pm5.17  860  pm5.6  880  orbidi  900  cador  1401  cadan  1402  19.30  1616  19.43  1617  nfor  1861  19.32  1900  dfsb3  2114  sbor  2144  neor  2695  r19.30  2860  r19.32v  2861  r19.43  2870  dfif2  3769  disjor  4227  sotric  4564  sotrieq  4565  isso2i  4570  soxp  6495  unxpwdom2  7592  cflim2  8181  cfpwsdom  8497  ltapr  8960  ltxrlt  9184  isprm4  13127  euclemma  13146  islpi  17251  restntr  17284  alexsubALTlem2  18117  alexsubALTlem3  18118  2bornot2b  21796  disjorf  24056  funcnv5mpt  24119  ballotlemodife  24790  3orit  25204  dfon2lem5  25449  ecase13d  26358  elicc3  26362  nn0prpw  26368  orfa  26734  unitresl  26737  cnf1dd  26745  tsim1  26754  tsbi3  26759  pm10.541  27651  r19.32  28033  sborNEW7  29740  dfsb3NEW7  29813
  Copyright terms: Public domain W3C validator