Definition df-or 848

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 28661). After we define the constant true ⊤ (df-tru 1546) and the constant false ⊥ (df-fal 1556), we will be able to prove these truth table values: ((⊤ ∨ ⊤) ↔ ⊤) (truortru 1580), ((⊤ ∨ ⊥) ↔ ⊤) (truorfal 1581), ((⊥ ∨ ⊤) ↔ ⊤) (falortru 1582), and ((⊥ ∨ ⊥) ↔ ⊥) (falorfal 1583).

Contrast with ∧ (df-an 400), → (wi 4), ⊼ (df-nan 1488), and ⊻ (df-xor 1508). (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 847	. 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 referenced by:  pm4.64  849  pm2.53  851  pm2.54  852  imor  853  ori  861  orri  862  ord  864  unitreslOLD  878  orbi2d  916  orimdi  931  orbidi  953  pm5.6  1002  ordi  1006  pm5.17  1012  nanbi  1496  cador  1615  nf4  1795  19.43  1890  nfor  1912  19.32v  1948  19.32  2233  sbor  2310  dfsb3  2499  neor  3036  r19.32v  3269  r19.43  3279  dfif2  4458  disjor  5050  soxp  7938  unxpwdom2  9252  cflim2  9925  cfpwsdom  10246  ltapr  10707  ltxrlt  10951  isprm4  16292  euclemma  16321  islpi  22183  restntr  22216  alexsubALTlem2  23082  alexsubALTlem3  23083  2bornot2b  28704  disjorf  30794  funcnv5mpt  30882  dvdszzq  31006  cycpm2tr  31263  ballotlemodife  32339  3orit  33535  dfon2lem5  33644  ecase13d  34404  elicc3  34408  nn0prpw  34414  onsucuni3  35444  orfa  36146  cnf1dd  36154  tsim1  36194  ineleq  36392  aks4d1p7  39997  isdomn5  40071  ifpidg  40968  ifpim123g  40977  ifpororb  40982  ifpor123g  40985  dfxor4  41236  df3or2  41238  frege83  41416  dffrege99  41432  frege131  41464  frege133  41466  pm10.541  41847  xrssre  42750  elprn2  43038  iundjiun  43861  r19.32  44450