Definition df-or 384

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 27408). After we define the constant true ⊤ (df-tru 1526) and the constant false ⊥ (df-fal 1529), we will be able to prove these truth table values: ((⊤ ∨ ⊤) ↔ ⊤) (truortru 1550), ((⊤ ∨ ⊥) ↔ ⊤) (truorfal 1551), ((⊥ ∨ ⊤) ↔ ⊤) (falortru 1552), and ((⊥ ∨ ⊥) ↔ ⊥) (falorfal 1553).

This is our first use of the biconditional connective in a definition; we use the biconditional connective in place of the traditional "<=def=>", which means the same thing, except that we can manipulate the biconditional connective directly in proofs rather than having to rely on an informal definition substitution rule. Note that if we mechanically substitute (¬ 𝜑 → 𝜓) for (𝜑 ∨ 𝜓), we end up with an instance of previously proved theorem biid 251. This is the justification for the definition, along with the fact that it introduces a new symbol ∨. Contrast with ∧ (df-an 385), → (wi 4), ⊼ (df-nan 1488), and ⊻ (df-xor 1505) . (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 382	. 2 wff (𝜑 ∨ 𝜓)
4	1	wn 3	. . 3 wff ¬ 𝜑
5	4, 2	wi 4	. 2 wff (¬ 𝜑 → 𝜓)
6	3, 5	wb 196	1 wff ((𝜑 ∨ 𝜓) ↔ (¬ 𝜑 → 𝜓))

This definition is referenced by:  pm4.64  386  pm2.53  387  pm2.54  388  ori  389  orri  390  ord  391  imor  427  mtord  693  orbi2d  738  orimdi  910  ordi  926  pm5.17  950  pm5.6  971  orbidi  993  nanbi  1494  cador  1587  nf4  1753  19.43  1850  nfor  1874  19.32v  1909  19.32  2139  nforOLD  2280  dfsb3  2402  sbor  2426  neor  2914  r19.30  3111  r19.32v  3112  r19.43  3122  dfif2  4121  disjor  4666  soxp  7335  unxpwdom2  8534  cflim2  9123  cfpwsdom  9444  ltapr  9905  ltxrlt  10146  isprm4  15444  euclemma  15472  islpi  21001  restntr  21034  alexsubALTlem2  21899  alexsubALTlem3  21900  2bornot2b  27450  disjorf  29518  funcnv5mpt  29597  ballotlemodife  30687  3orit  31722  dfon2lem5  31816  ecase13d  32432  elicc3  32436  nn0prpw  32443  onsucuni3  33345  orfa  34011  unitresl  34014  cnf1dd  34022  tsim1  34067  ineleq  34259  ifpidg  38153  ifpim123g  38162  ifpororb  38167  ifpor123g  38170  dfxor4  38375  df3or2  38377  frege83  38557  dffrege99  38573  frege131  38605  frege133  38607  pm10.541  38883  xrssre  39877  elprn2  40184  iundjiun  40995  r19.32  41488