Definition df-or 847

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 29674). After we define the constant true ⊤ (df-tru 1545) and the constant false ⊥ (df-fal 1555), we will be able to prove these truth table values: ((⊤ ∨ ⊤) ↔ ⊤) (truortru 1579), ((⊤ ∨ ⊥) ↔ ⊤) (truorfal 1580), ((⊥ ∨ ⊤) ↔ ⊤) (falortru 1581), and ((⊥ ∨ ⊥) ↔ ⊥) (falorfal 1582).

Contrast with ∧ (df-an 398), → (wi 4), ⊼ (df-nan 1491), and ⊻ (df-xor 1511). (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 846	. 2 wff (𝜑 ∨ 𝜓)
4	1	wn 3	. . 3 wff ¬ 𝜑
5	4, 2	wi 4	. 2 wff (¬ 𝜑 → 𝜓)
6	3, 5	wb 205	1 wff ((𝜑 ∨ 𝜓) ↔ (¬ 𝜑 → 𝜓))

This definition is referenced by:  pm4.64  848  pm2.53  850  pm2.54  851  imor  852  ori  860  orri  861  ord  863  unitreslOLD  877  orbi2d  915  orimdi  930  orbidi  952  pm5.6  1001  ordi  1005  pm5.17  1011  nanbi  1499  cador  1610  nf4  1790  19.43  1886  nfor  1908  19.32v  1944  19.32  2227  sbor  2304  dfsb3  2494  neor  3035  r19.43  3123  r19.32v  3192  dfif2  4531  disjor  5129  soxp  8115  unxpwdom2  9583  cflim2  10258  cfpwsdom  10579  ltapr  11040  ltxrlt  11284  isprm4  16621  euclemma  16650  isdomn5  20917  islpi  22653  restntr  22686  alexsubALTlem2  23552  alexsubALTlem3  23553  2bornot2b  29717  disjorf  31810  funcnv5mpt  31893  dvdszzq  32021  cycpm2tr  32278  ballotlemodife  33496  3orit  34685  dfon2lem5  34759  ecase13d  35198  elicc3  35202  nn0prpw  35208  onsucuni3  36248  orfa  36950  cnf1dd  36958  tsim1  36998  ineleq  37223  aks4d1p7  40948  safesnsupfilb  42169  ifpidg  42242  ifpim123g  42251  ifpororb  42256  ifpor123g  42259  dfxor4  42517  df3or2  42519  frege83  42697  dffrege99  42713  frege131  42745  frege133  42747  pm10.541  43126  xrssre  44058  elprn2  44350  iundjiun  45176  r19.32  45806