Definition df-or 861

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 30738). After we define the constant true ⊤ (df-tru 1571) and the constant false ⊥ (df-fal 1581), we will be able to prove these truth table values: ((⊤ ∨ ⊤) ↔ ⊤) (truortru 1605), ((⊤ ∨ ⊥) ↔ ⊤) (truorfal 1606), ((⊥ ∨ ⊤) ↔ ⊤) (falortru 1607), and ((⊥ ∨ ⊥) ↔ ⊥) (falorfal 1608).

Contrast with ∧ (df-an 401), → (wi 4), ⊼ (df-nan 1520), and ⊻ (df-xor 1540). (Contributed by NM, 27-Dec-1992.)

Assertion

Ref	Expression
df-or	⊢ ((𝜑 ∨ 𝜓) ↔ (¬ 𝜑 → 𝜓))

Detailed syntax breakdown of Definition df-or

Step	Hyp	Ref	Expression
1		wph	. . 3 wff 𝜑
2		wps	. . 3 wff 𝜓
3	1, 2	wo 860	. 2 wff (𝜑 ∨ 𝜓)
4	1	wn 3	. . 3 wff ¬ 𝜑
5	4, 2	wi 4	. 2 wff (¬ 𝜑 → 𝜓)
6	3, 5	wb 209	1 wff ((𝜑 ∨ 𝜓) ↔ (¬ 𝜑 → 𝜓))

This definition is referenced by:  pm4.64  862  pm2.53  864  pm2.54  865  imor  866  ori  874  orri  875  ord  877  orbi2d  928  orimdi  943  orbidi  967  pm5.6  1017  ordi  1021  pm5.17  1027  ecase13d  1500  nanbi  1528  cador  1636  nf4  1815  19.43  1910  nfor  1932  19.32v  1968  19.32  2267  sbor  2339  dfsb3  2524  neor  3048  r19.43  3131  r19.32v  3196  dfif2  4488  disjor  5090  soxp  8124  unxpwdom2  9549  cflim2  10246  cfpwsdom  10568  ltapr  11029  ltxrlt  11279  isprm4  16741  euclemma  16771  dvdszzq  16779  isdomn5  20794  islpi  23285  restntr  23318  alexsubALTlem2  24184  alexsubALTlem3  24185  elplng  29036  plngcplem  29041  plngrotlem2  29044  2bornot2b  30781  disjorf  32890  funcnv5mpt  32978  cycpm2tr  33405  ballotlemodife  34854  orbi2iALT  36131  3orit  36162  dfon2lem5  36231  elicc3  36772  nn0prpw  36778  onsucuni3  37957  orfa  38677  cnf1dd  38685  tsim1  38725  ineleq  38949  aks4d1p7  42796  safesnsupfilb  44092  ifpidg  44165  ifpim123g  44174  ifpororb  44179  ifpor123g  44182  dfxor4  44440  df3or2  44442  frege83  44620  dffrege99  44636  frege131  44668  frege133  44670  pm10.541  45025  xrssre  46012  iundjiun  47122  r19.32  47780