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 29654). 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  4529  disjor  5127  soxp  8110  unxpwdom2  9579  cflim2  10254  cfpwsdom  10575  ltapr  11036  ltxrlt  11280  isprm4  16617  euclemma  16646  islpi  22635  restntr  22668  alexsubALTlem2  23534  alexsubALTlem3  23535  2bornot2b  29697  disjorf  31788  funcnv5mpt  31871  dvdszzq  31999  cycpm2tr  32256  ballotlemodife  33434  3orit  34623  dfon2lem5  34697  ecase13d  35136  elicc3  35140  nn0prpw  35146  onsucuni3  36186  orfa  36888  cnf1dd  36896  tsim1  36936  ineleq  37161  aks4d1p7  40886  isdomn5  40969  safesnsupfilb  42102  ifpidg  42175  ifpim123g  42184  ifpororb  42189  ifpor123g  42192  dfxor4  42450  df3or2  42452  frege83  42630  dffrege99  42646  frege131  42678  frege133  42680  pm10.541  43059  xrssre  43993  elprn2  44285  iundjiun  45111  r19.32  45741