Definition df-or 845

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 28206). After we define the constant true ⊤ (df-tru 1541) and the constant false ⊥ (df-fal 1551), we will be able to prove these truth table values: ((⊤ ∨ ⊤) ↔ ⊤) (truortru 1575), ((⊤ ∨ ⊥) ↔ ⊤) (truorfal 1576), ((⊥ ∨ ⊤) ↔ ⊤) (falortru 1577), and ((⊥ ∨ ⊥) ↔ ⊥) (falorfal 1578).

Contrast with ∧ (df-an 400), → (wi 4), ⊼ (df-nan 1483), and ⊻ (df-xor 1503). (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 844	. 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  846  pm2.53  848  pm2.54  849  imor  850  ori  858  orri  859  ord  861  unitreslOLD  875  orbi2d  913  orimdi  928  orbidi  950  pm5.6  999  ordi  1003  pm5.17  1009  nanbi  1491  cador  1610  nf4  1789  19.43  1883  nfor  1905  19.32v  1941  19.32  2233  sbor  2312  dfsb3  2512  dfsb3ALT  2568  neor  3078  r19.32v  3294  r19.43  3304  dfif2  4427  disjor  5010  soxp  7806  unxpwdom2  9036  cflim2  9674  cfpwsdom  9995  ltapr  10456  ltxrlt  10700  isprm4  16018  euclemma  16047  islpi  21754  restntr  21787  alexsubALTlem2  22653  alexsubALTlem3  22654  2bornot2b  28249  disjorf  30342  funcnv5mpt  30431  dvdszzq  30557  cycpm2tr  30811  ballotlemodife  31865  3orit  33058  dfon2lem5  33145  ecase13d  33774  elicc3  33778  nn0prpw  33784  onsucuni3  34784  orfa  35520  cnf1dd  35528  tsim1  35568  ineleq  35768  ifpidg  40199  ifpim123g  40208  ifpororb  40213  ifpor123g  40216  dfxor4  40467  df3or2  40469  frege83  40647  dffrege99  40663  frege131  40695  frege133  40697  pm10.541  41071  xrssre  41980  elprn2  42276  iundjiun  43099  r19.32  43653