Definition df-or 849

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 30514). 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 396), → (wi 4), ⊼ (df-nan 1494), and ⊻ (df-xor 1514). (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 848	. 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  850  pm2.53  852  pm2.54  853  imor  854  ori  862  orri  863  ord  865  orbi2d  916  orimdi  931  orbidi  955  pm5.6  1004  ordi  1008  pm5.17  1014  nanbi  1502  cador  1610  nf4  1789  19.43  1884  nfor  1906  19.32v  1942  19.32  2241  sbor  2313  dfsb3  2499  neor  3025  r19.43  3106  r19.32v  3171  dfif2  4483  disjor  5082  soxp  8083  unxpwdom2  9507  cflim2  10187  cfpwsdom  10509  ltapr  10970  ltxrlt  11217  isprm4  16625  euclemma  16654  dvdszzq  16662  isdomn5  20660  islpi  23110  restntr  23143  alexsubALTlem2  24009  alexsubALTlem3  24010  2bornot2b  30557  disjorf  32672  funcnv5mpt  32763  cycpm2tr  33219  ballotlemodife  34682  orbi2iALT  35907  3orit  35938  dfon2lem5  36007  ecase13d  36535  elicc3  36539  nn0prpw  36545  onsucuni3  37649  orfa  38362  cnf1dd  38370  tsim1  38410  ineleq  38634  aks4d1p7  42482  safesnsupfilb  43803  ifpidg  43876  ifpim123g  43885  ifpororb  43890  ifpor123g  43893  dfxor4  44151  df3or2  44153  frege83  44331  dffrege99  44347  frege131  44379  frege133  44381  pm10.541  44752  xrssre  45736  iundjiun  46847  r19.32  47487