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

Contrast with ∧ (df-an 402), → (wi 4), ⊼ (df-nan 1522), and ⊻ (df-xor 1542). (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  1503  nanbi  1530  cador  1641  nf4  1820  19.43  1917  nfor  1939  19.32v  1975  19.32  2273  sbor  2343  dfsb3  2526  neor  3051  r19.43  3134  r19.32v  3199  dfif2  4487  disjor  5088  soxp  8165  unxpwdom2  9606  cflim2  10365  cfpwsdom  10693  ltapr  11154  ltxrlt  11404  isprm4  16885  euclemma  16915  dvdszzq  16923  isdomn5  20989  islpi  23494  restntr  23527  alexsubALTlem2  24394  alexsubALTlem3  24395  elplng  29285  plngcplem  29290  plngrotlem2  29293  2bornot2b  31092  disjorf  33242  funcnv5mpt  33330  cycpm2tr  33747  ballotlemodife  35197  orbi2iALT  36616  3orit  36658  dfon2lem5  36726  elicc3  37282  nn0prpw  37288  onsucuni3  38481  orfa  39207  cnf1dd  39213  tsim1  39253  ineleq  39477  aks4d1p7  43324  safesnsupfilb  44609  ifpidg  44682  ifpim123g  44691  ifpororb  44696  ifpor123g  44699  dfxor4  44956  df3or2  44958  frege83  45136  dffrege99  45152  frege131  45184  frege133  45186  pm10.541  45541  xrssre  46563  iundjiun  47673  r19.32  48372