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 1542) and the constant false ⊥ (df-fal 1552), we will be able to prove these truth table values: ((⊤ ∨ ⊤) ↔ ⊤) (truortru 1576), ((⊤ ∨ ⊥) ↔ ⊤) (truorfal 1577), ((⊥ ∨ ⊤) ↔ ⊤) (falortru 1578), and ((⊥ ∨ ⊥) ↔ ⊥) (falorfal 1579).

Contrast with ∧ (df-an 396), → (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 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  1499  cador  1607  nf4  1786  19.43  1881  nfor  1903  19.32v  1939  19.32  2232  sbor  2306  dfsb3  2497  neor  3023  r19.43  3109  r19.32v  3179  dfif2  4509  disjor  5107  soxp  8137  unxpwdom2  9611  cflim2  10286  cfpwsdom  10607  ltapr  11068  ltxrlt  11314  isprm4  16704  euclemma  16733  dvdszzq  16741  isdomn5  20679  islpi  23118  restntr  23151  alexsubALTlem2  24017  alexsubALTlem3  24018  2bornot2b  30426  disjorf  32535  funcnv5mpt  32621  cycpm2tr  33081  ballotlemodife  34437  orbi2iALT  35627  3orit  35653  dfon2lem5  35725  ecase13d  36251  elicc3  36255  nn0prpw  36261  onsucuni3  37305  orfa  38026  cnf1dd  38034  tsim1  38074  ineleq  38292  aks4d1p7  42021  safesnsupfilb  43372  ifpidg  43445  ifpim123g  43454  ifpororb  43459  ifpor123g  43462  dfxor4  43720  df3or2  43722  frege83  43900  dffrege99  43916  frege131  43948  frege133  43950  pm10.541  44327  xrssre  45300  elprn2  45590  iundjiun  46416  r19.32  47052