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 30885). 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  2271  sbor  2341  dfsb3  2525  neor  3049  r19.43  3132  r19.32v  3197  dfif2  4487  disjor  5089  soxp  8130  unxpwdom2  9563  cflim2  10268  cfpwsdom  10594  ltapr  11055  ltxrlt  11305  isprm4  16776  euclemma  16806  dvdszzq  16814  isdomn5  20871  islpi  23373  restntr  23406  alexsubALTlem2  24273  alexsubALTlem3  24274  elplng  29133  plngcplem  29138  plngrotlem2  29141  2bornot2b  30928  disjorf  33037  funcnv5mpt  33125  cycpm2tr  33544  ballotlemodife  34994  orbi2iALT  36249  3orit  36280  dfon2lem5  36349  elicc3  36921  nn0prpw  36927  onsucuni3  38106  orfa  38817  cnf1dd  38823  tsim1  38863  ineleq  39087  aks4d1p7  42934  safesnsupfilb  44243  ifpidg  44316  ifpim123g  44325  ifpororb  44330  ifpor123g  44333  dfxor4  44591  df3or2  44593  frege83  44771  dffrege99  44787  frege131  44819  frege133  44821  pm10.541  45176  xrssre  46163  iundjiun  47273  r19.32  47971