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 30955). 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  2269  sbor  2339  dfsb3  2523  neor  3047  r19.43  3130  r19.32v  3195  dfif2  4483  disjor  5084  soxp  8124  unxpwdom2  9560  cflim2  10312  cfpwsdom  10640  ltapr  11101  ltxrlt  11351  isprm4  16821  euclemma  16851  dvdszzq  16859  isdomn5  20923  islpi  23428  restntr  23461  alexsubALTlem2  24328  alexsubALTlem3  24329  elplng  29191  plngcplem  29196  plngrotlem2  29199  2bornot2b  30998  disjorf  33106  funcnv5mpt  33194  cycpm2tr  33613  ballotlemodife  35064  orbi2iALT  36371  3orit  36402  dfon2lem5  36471  elicc3  37027  nn0prpw  37033  onsucuni3  38210  orfa  38936  cnf1dd  38942  tsim1  38982  ineleq  39206  aks4d1p7  43053  safesnsupfilb  44362  ifpidg  44435  ifpim123g  44444  ifpororb  44449  ifpor123g  44452  dfxor4  44710  df3or2  44712  frege83  44890  dffrege99  44906  frege131  44938  frege133  44940  pm10.541  45295  xrssre  46282  iundjiun  47392  r19.32  48090