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 30488). 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  4469  disjor  5068  soxp  8076  unxpwdom2  9500  cflim2  10182  cfpwsdom  10504  ltapr  10965  ltxrlt  11213  isprm4  16650  euclemma  16680  dvdszzq  16688  isdomn5  20684  islpi  23111  restntr  23144  alexsubALTlem2  24010  alexsubALTlem3  24011  2bornot2b  30531  disjorf  32646  funcnv5mpt  32737  cycpm2tr  33177  ballotlemodife  34639  orbi2iALT  35864  3orit  35895  dfon2lem5  35964  ecase13d  36492  elicc3  36496  nn0prpw  36502  onsucuni3  37680  orfa  38400  cnf1dd  38408  tsim1  38448  ineleq  38672  aks4d1p7  42519  safesnsupfilb  43842  ifpidg  43915  ifpim123g  43924  ifpororb  43929  ifpor123g  43932  dfxor4  44190  df3or2  44192  frege83  44370  dffrege99  44386  frege131  44418  frege133  44420  pm10.541  44791  xrssre  45775  iundjiun  46885  r19.32  47537