Definition df-or 370

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 (ex-or 25142). After we define the constant true (df-tru 1398) and the constant false (df-fal 1401), we will be able to prove these truth table values: (truortru 1423), (truorfal 1424), (falortru 1425), and (falorfal 1426).

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 236. This is the justification for the definition, along with the fact that it introduces a new symbol \/. Contrast with /\ (df-an 371), -> (wi 4), -/\ (df-nan 1344), and \/_ (df-xor 1364) . (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
2		wps	. . 3
3	1, 2	wo 368	. 2
4	1	wn 3	. . 3
5	4, 2	wi 4	. 2
6	3, 5	wb 184	1

This definition is referenced by:  pm4.64  372  pm2.53  373  pm2.54  374  ori  375  orri  376  ord  377  imor  412  mtord  660  orbi2d  701  orimdi  847  ordi  864  pm5.17  888  pm5.6  912  orbidi  932  nanbi  1352  cador  1458  19.43  1693  19.32v  1730  nfor  1935  19.32  1967  dfsb3  2115  sbor  2139  neor  2781  r19.30  3002  r19.32v  3003  r19.43  3013  dfif2  3943  disjor  4436  sotric  4831  sotrieq  4832  isso2i  4837  soxp  6913  unxpwdom2  8035  cflim2  8664  cfpwsdom  8980  ltapr  9444  ltxrlt  9676  isprm4  14227  euclemma  14249  islpi  19650  restntr  19683  alexsubALTlem2  20548  alexsubALTlem3  20549  2bornot2b  25172  disjorf  27440  funcnv5mpt  27511  ballotlemodife  28436  3orit  29092  dfon2lem5  29219  ecase13d  30131  elicc3  30135  nn0prpw  30141  orfa  30479  unitresl  30482  cnf1dd  30490  tsim1  30537  pm10.541  31272  elprn2  31640  r19.32  32172  bj-ifim123g  37706  bj-ifidg  37707  bj-ifor123g  37725  bj-ifororb  37726  dfxor4  37789