Definition df-or 847

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

Contrast with ∧ (df-an 396), → (wi 4), ⊼ (df-nan 1489), and ⊻ (df-xor 1509). (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 846	. 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  848  pm2.53  850  pm2.54  851  imor  852  ori  860  orri  861  ord  863  orbi2d  914  orimdi  929  orbidi  953  pm5.6  1002  ordi  1006  pm5.17  1012  nanbi  1497  cador  1605  nf4  1785  19.43  1881  nfor  1903  19.32v  1939  19.32  2234  sbor  2311  dfsb3  2502  neor  3040  r19.43  3128  r19.32v  3198  dfif2  4550  disjor  5148  soxp  8170  unxpwdom2  9657  cflim2  10332  cfpwsdom  10653  ltapr  11114  ltxrlt  11360  isprm4  16731  euclemma  16760  dvdszzq  16768  isdomn5  20732  islpi  23178  restntr  23211  alexsubALTlem2  24077  alexsubALTlem3  24078  2bornot2b  30496  disjorf  32601  funcnv5mpt  32686  cycpm2tr  33112  ballotlemodife  34462  orbi2iALT  35653  3orit  35678  dfon2lem5  35751  ecase13d  36279  elicc3  36283  nn0prpw  36289  onsucuni3  37333  orfa  38042  cnf1dd  38050  tsim1  38090  ineleq  38310  aks4d1p7  42040  safesnsupfilb  43380  ifpidg  43453  ifpim123g  43462  ifpororb  43467  ifpor123g  43470  dfxor4  43728  df3or2  43730  frege83  43908  dffrege99  43924  frege131  43956  frege133  43958  pm10.541  44336  xrssre  45263  elprn2  45555  iundjiun  46381  r19.32  47013