Definition df-or 862

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

Contrast with ∧ (df-an 402), → (wi 4), ⊼ (df-nan 1521), and ⊻ (df-xor 1541). (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 861	. 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 used by:  pm4.64  863  pm2.53  865  pm2.54  866  imor  867  ori  875  orri  876  ord  878  orbi2d  929  orimdi  944  orbidi  967  pm5.6  1017  ordi  1023  pm5.17  1029  ecase13d  1502  nanbi  1529  cador  1640  nf4  1819  19.43  1914  nfor  1936  19.32v  1972  19.32  2269  sbor  2339  dfsb3  2523  neor  3047  r19.43  3130  r19.32v  3195  dfif2  4483  disjor  5084  soxp  8141  unxpwdom2  9582  cflim2  10341  cfpwsdom  10669  ltapr  11130  ltxrlt  11380  isprm4  16859  euclemma  16889  dvdszzq  16897  isdomn5  20962  islpi  23467  restntr  23500  alexsubALTlem2  24367  alexsubALTlem3  24368  elplng  29258  plngcplem  29263  plngrotlem2  29266  2bornot2b  31065  disjorf  33215  funcnv5mpt  33303  cycpm2tr  33722  ballotlemodife  35172  orbi2iALT  36492  3orit  36523  dfon2lem5  36591  elicc3  37147  nn0prpw  37153  onsucuni3  38333  orfa  39059  cnf1dd  39065  tsim1  39105  ineleq  39329  aks4d1p7  43176  safesnsupfilb  44461  ifpidg  44534  ifpim123g  44543  ifpororb  44548  ifpor123g  44551  dfxor4  44808  df3or2  44810  frege83  44988  dffrege99  45004  frege131  45036  frege133  45038  pm10.541  45393  xrssre  46402  iundjiun  47512  r19.32  48210