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 30479). 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  2240  sbor  2312  dfsb3  2497  neor  3022  r19.43  3103  r19.32v  3168  dfif2  4458  disjor  5056  soxp  8068  unxpwdom2  9492  cflim2  10174  cfpwsdom  10496  ltapr  10957  ltxrlt  11205  isprm4  16642  euclemma  16672  dvdszzq  16680  isdomn5  20676  islpi  23102  restntr  23135  alexsubALTlem2  24001  alexsubALTlem3  24002  2bornot2b  30522  disjorf  32637  funcnv5mpt  32728  cycpm2tr  33168  ballotlemodife  34630  orbi2iALT  35855  3orit  35886  dfon2lem5  35955  ecase13d  36483  elicc3  36487  nn0prpw  36493  onsucuni3  37671  orfa  38391  cnf1dd  38399  tsim1  38439  ineleq  38663  aks4d1p7  42510  safesnsupfilb  43833  ifpidg  43906  ifpim123g  43915  ifpororb  43920  ifpor123g  43923  dfxor4  44181  df3or2  44183  frege83  44361  dffrege99  44377  frege131  44409  frege133  44411  pm10.541  44782  xrssre  45766  iundjiun  46876  r19.32  47534