Definition df-or 849

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 30500). After we define the constant true ⊤ (df-tru 1545) and the constant false ⊥ (df-fal 1555), we will be able to prove these truth table values: ((⊤ ∨ ⊤) ↔ ⊤) (truortru 1579), ((⊤ ∨ ⊥) ↔ ⊤) (truorfal 1580), ((⊥ ∨ ⊤) ↔ ⊤) (falortru 1581), and ((⊥ ∨ ⊥) ↔ ⊥) (falorfal 1582).

Contrast with ∧ (df-an 396), → (wi 4), ⊼ (df-nan 1494), and ⊻ (df-xor 1514). (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 848	. 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  850  pm2.53  852  pm2.54  853  imor  854  ori  862  orri  863  ord  865  orbi2d  916  orimdi  931  orbidi  955  pm5.6  1004  ordi  1008  pm5.17  1014  nanbi  1502  cador  1610  nf4  1789  19.43  1884  nfor  1906  19.32v  1942  19.32  2241  sbor  2313  dfsb3  2499  neor  3025  r19.43  3105  r19.32v  3170  dfif2  4482  disjor  5081  soxp  8073  unxpwdom2  9497  cflim2  10177  cfpwsdom  10499  ltapr  10960  ltxrlt  11207  isprm4  16615  euclemma  16644  dvdszzq  16652  isdomn5  20647  islpi  23097  restntr  23130  alexsubALTlem2  23996  alexsubALTlem3  23997  2bornot2b  30543  disjorf  32657  funcnv5mpt  32748  cycpm2tr  33203  ballotlemodife  34657  orbi2iALT  35881  3orit  35912  dfon2lem5  35981  ecase13d  36509  elicc3  36513  nn0prpw  36519  onsucuni3  37574  orfa  38285  cnf1dd  38293  tsim1  38333  ineleq  38557  aks4d1p7  42405  safesnsupfilb  43726  ifpidg  43799  ifpim123g  43808  ifpororb  43813  ifpor123g  43816  dfxor4  44074  df3or2  44076  frege83  44254  dffrege99  44270  frege131  44302  frege133  44304  pm10.541  44675  xrssre  45660  iundjiun  46771  r19.32  47411