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

Contrast with ∧ (df-an 396), → (wi 4), ⊼ (df-nan 1493), and ⊻ (df-xor 1513). (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 206	1 wff ((𝜑 ∨ 𝜓) ↔ (¬ 𝜑 → 𝜓))

This definition is referenced by:  pm4.64  849  pm2.53  851  pm2.54  852  imor  853  ori  861  orri  862  ord  864  orbi2d  915  orimdi  930  orbidi  954  pm5.6  1003  ordi  1007  pm5.17  1013  nanbi  1501  cador  1609  nf4  1788  19.43  1883  nfor  1905  19.32v  1941  19.32  2236  sbor  2308  dfsb3  2494  neor  3020  r19.43  3100  r19.32v  3165  dfif2  4477  disjor  5073  soxp  8059  unxpwdom2  9474  cflim2  10151  cfpwsdom  10472  ltapr  10933  ltxrlt  11180  isprm4  16592  euclemma  16621  dvdszzq  16629  isdomn5  20623  islpi  23062  restntr  23095  alexsubALTlem2  23961  alexsubALTlem3  23962  2bornot2b  30439  disjorf  32554  funcnv5mpt  32645  cycpm2tr  33083  ballotlemodife  34506  orbi2iALT  35717  3orit  35748  dfon2lem5  35820  ecase13d  36346  elicc3  36350  nn0prpw  36356  onsucuni3  37400  orfa  38121  cnf1dd  38129  tsim1  38169  ineleq  38381  aks4d1p7  42115  safesnsupfilb  43450  ifpidg  43523  ifpim123g  43532  ifpororb  43537  ifpor123g  43540  dfxor4  43798  df3or2  43800  frege83  43978  dffrege99  43994  frege131  44026  frege133  44028  pm10.541  44399  xrssre  45386  iundjiun  46497  r19.32  47128