Definition df-or 862

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 30809). After we define the constant true ⊤ (df-tru 1573) and the constant false ⊥ (df-fal 1583), we will be able to prove these truth table values: ((⊤ ∨ ⊤) ↔ ⊤) (truortru 1607), ((⊤ ∨ ⊥) ↔ ⊤) (truorfal 1608), ((⊥ ∨ ⊤) ↔ ⊤) (falortru 1609), and ((⊥ ∨ ⊥) ↔ ⊥) (falorfal 1610).

Contrast with ∧ (df-an 402), → (wi 4), ⊼ (df-nan 1522), and ⊻ (df-xor 1542). (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 861	. 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 used by:  pm4.64  863  pm2.53  865  pm2.54  866  imor  867  ori  875  orri  876  ord  878  orbi2d  929  orimdi  944  orbidi  967  pm5.6  1017  ordi  1023  pm5.17  1029  ecase13d  1502  nanbi  1530  cador  1641  nf4  1820  19.43  1915  nfor  1937  19.32v  1973  19.32  2272  sbor  2344  dfsb3  2529  neor  3053  r19.43  3136  r19.32v  3201  dfif2  4494  disjor  5096  soxp  8134  unxpwdom2  9560  cflim2  10265  cfpwsdom  10587  ltapr  11048  ltxrlt  11298  isprm4  16767  euclemma  16797  dvdszzq  16805  isdomn5  20846  islpi  23343  restntr  23376  alexsubALTlem2  24242  alexsubALTlem3  24243  elplng  29099  plngcplem  29104  plngrotlem2  29107  2bornot2b  30852  disjorf  32961  funcnv5mpt  33049  cycpm2tr  33470  ballotlemodife  34919  orbi2iALT  36197  3orit  36228  dfon2lem5  36297  elicc3  36868  nn0prpw  36874  onsucuni3  38053  orfa  38773  cnf1dd  38779  tsim1  38819  ineleq  39043  aks4d1p7  42890  safesnsupfilb  44184  ifpidg  44257  ifpim123g  44266  ifpororb  44271  ifpor123g  44274  dfxor4  44532  df3or2  44534  frege83  44712  dffrege99  44728  frege131  44760  frege133  44762  pm10.541  45117  xrssre  46104  iundjiun  47214  r19.32  47875