Definition df-or 837

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 27853). After we define the constant true ⊤ (df-tru 1605) and the constant false ⊥ (df-fal 1615), we will be able to prove these truth table values: ((⊤ ∨ ⊤) ↔ ⊤) (truortru 1639), ((⊤ ∨ ⊥) ↔ ⊤) (truorfal 1640), ((⊥ ∨ ⊤) ↔ ⊤) (falortru 1641), and ((⊥ ∨ ⊥) ↔ ⊥) (falorfal 1642).

Contrast with ∧ (df-an 387), → (wi 4), ⊼ (df-nan 1558), and ⊻ (df-xor 1583). (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 836	. 2 wff (𝜑 ∨ 𝜓)
4	1	wn 3	. . 3 wff ¬ 𝜑
5	4, 2	wi 4	. 2 wff (¬ 𝜑 → 𝜓)
6	3, 5	wb 198	1 wff ((𝜑 ∨ 𝜓) ↔ (¬ 𝜑 → 𝜓))

This definition is referenced by:  pm4.64  838  pm2.53  840  pm2.54  841  imor  842  ori  850  orri  851  ord  853  mtord  866  orbi2d  902  orimdi  917  orbidi  938  pm5.6  987  ordi  991  pm5.17  997  nanbi  1569  cador  1666  nf4  1831  19.43  1929  nfor  1951  19.32v  1983  19.32  2219  dfsb3  2450  sbor  2474  neor  3061  r19.30  3268  r19.32v  3269  r19.43  3279  dfif2  4309  disjor  4868  soxp  7571  unxpwdom2  8782  cflim2  9420  cfpwsdom  9741  ltapr  10202  ltxrlt  10447  isprm4  15802  euclemma  15829  islpi  21361  restntr  21394  alexsubALTlem2  22260  alexsubALTlem3  22261  2bornot2b  27895  disjorf  29955  funcnv5mpt  30033  ballotlemodife  31158  3orit  32193  dfon2lem5  32280  ecase13d  32896  elicc3  32900  nn0prpw  32906  onsucuni3  33810  orfa  34505  unitresl  34508  cnf1dd  34515  tsim1  34559  ineleq  34747  ifpidg  38794  ifpim123g  38803  ifpororb  38808  ifpor123g  38811  dfxor4  39015  df3or2  39017  frege83  39196  dffrege99  39212  frege131  39244  frege133  39246  pm10.541  39522  xrssre  40472  elprn2  40774  iundjiun  41601  r19.32  42126