Definition df-or 848

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

Contrast with ∧ (df-an 396), → (wi 4), ⊼ (df-nan 1492), and ⊻ (df-xor 1512). (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 847	. 2 wff (𝜑 ∨ 𝜓)
4	1	wn 3	. . 3 wff ¬ 𝜑
5	4, 2	wi 4	. 2 wff (¬ 𝜑 → 𝜓)
6	3, 5	wb 206	1 wff ((𝜑 ∨ 𝜓) ↔ (¬ 𝜑 → 𝜓))

This definition is referenced by:  pm4.64  849  pm2.53  851  pm2.54  852  imor  853  ori  861  orri  862  ord  864  orbi2d  915  orimdi  930  orbidi  954  pm5.6  1003  ordi  1007  pm5.17  1013  nanbi  1500  cador  1608  nf4  1787  19.43  1882  nfor  1904  19.32v  1940  19.32  2234  sbor  2306  dfsb3  2492  neor  3017  r19.43  3097  r19.32v  3162  dfif2  4480  disjor  5077  soxp  8069  unxpwdom2  9499  cflim2  10176  cfpwsdom  10497  ltapr  10958  ltxrlt  11204  isprm4  16613  euclemma  16642  dvdszzq  16650  isdomn5  20613  islpi  23052  restntr  23085  alexsubALTlem2  23951  alexsubALTlem3  23952  2bornot2b  30426  disjorf  32541  funcnv5mpt  32625  cycpm2tr  33074  ballotlemodife  34465  orbi2iALT  35657  3orit  35688  dfon2lem5  35760  ecase13d  36286  elicc3  36290  nn0prpw  36296  onsucuni3  37340  orfa  38061  cnf1dd  38069  tsim1  38109  ineleq  38321  aks4d1p7  42056  safesnsupfilb  43391  ifpidg  43464  ifpim123g  43473  ifpororb  43478  ifpor123g  43481  dfxor4  43739  df3or2  43741  frege83  43919  dffrege99  43935  frege131  43967  frege133  43969  pm10.541  44340  xrssre  45328  elprn2  45616  iundjiun  46442  r19.32  47083