Definition df-or 361

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 22750). After we define the constant true (df-tru 1338) and the constant false (df-fal 1339), we will be able to prove these truth table values: (truortru 1359), (truorfal 1360), (falortru 1361), and (falorfal 1362).

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 229. This is the justification for the definition, along with the fact that it introduces a new symbol \/. Contrast with /\ (df-an 362), -> (wi 4), -/\ (df-nan 1305), and \/_ (df-xor 1322) . (Contributed by NM, 5-Aug-1993.)

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 359	. 2
4	1	wn 3	. . 3
5	4, 2	wi 4	. 2
6	3, 5	wb 178	1

This definition is referenced by:  pm4.64  363  pm2.53  364  pm2.54  365  ori  366  orri  367  ord  368  imor  403  mtord  643  orbi2d  684  orimdi  822  ordi  836  pm5.17  860  pm5.6  880  orbidi  900  cador  1410  cadanOLD  1412  19.30  1632  19.43  1633  nfor  1862  19.32  1900  dfsb3  2119  sbor  2148  neor  2741  r19.30  2908  r19.32v  2909  r19.43  2919  dfif2  3827  disjor  4302  sotric  4688  sotrieq  4689  isso2i  4694  soxp  6691  unxpwdom2  7723  cflim2  8314  cfpwsdom  8630  ltapr  9093  ltxrlt  9324  fzocatel  11454  isprm4  13620  euclemma  13641  islpi  18227  restntr  18260  alexsubALTlem2  19094  alexsubALTlem3  19095  2bornot2b  22779  disjorf  25051  funcnv5mpt  25118  ballotlemodife  26030  sgn3da  26074  3orit  26511  dfon2lem5  26753  ecase13d  27688  elicc3  27692  nn0prpw  27698  orfa  28064  unitresl  28067  cnf1dd  28075  tsim1  28084  tsbi3  28089  pm10.541  28793  r19.32  29170  sborNEW11  31118  dfsb3NEW11  31190