Definition df-or 371

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 25869). After we define the constant true T. (df-tru 1440) and the constant false F. (df-fal 1443), we will be able to prove these truth table values: ( ( T. \/ T. ) <-> T. ) (truortru 1463), ( ( T. \/ F. ) <-> T. ) (truorfal 1464), ( ( F. \/ T. ) <-> T. ) (falortru 1465), and ( ( F. \/ F. ) <-> F. ) (falorfal 1466).

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 ( -. ph -> ps ) for ( ph \/ ps ), we end up with an instance of previously proved theorem biid 239. This is the justification for the definition, along with the fact that it introduces a new symbol \/. Contrast with /\ (df-an 372), -> (wi 4), -/\ (df-nan 1380), and \/_ (df-xor 1401) . (Contributed by NM, 27-Dec-1992.)

Assertion

Ref	Expression
df-or	|- ( ( ph \/ ps ) <-> ( -. ph -> ps ) )

Detailed syntax breakdown of Definition df-or

Step	Hyp	Ref	Expression
1		wph	. . 3 wff ph
2		wps	. . 3 wff ps
3	1, 2	wo 369	. 2 wff ( ph \/ ps )
4	1	wn 3	. . 3 wff -. ph
5	4, 2	wi 4	. 2 wff ( -. ph -> ps )
6	3, 5	wb 187	1 wff ( ( ph \/ ps ) <-> ( -. ph -> ps ) )

This definition is referenced by:  pm4.64  373  pm2.53  374  pm2.54  375  ori  376  orri  377  ord  378  imor  413  mtord  664  orbi2d  706  orimdi  855  ordi  872  pm5.17  896  pm5.6  920  orbidi  940  nanbi  1388  nanbiOLD  1389  cador  1504  19.43  1739  19.32v  1782  nfor  1995  19.32  2026  dfsb3  2172  sbor  2196  neor  2744  r19.30  2970  r19.32v  2971  r19.43  2981  dfif2  3913  disjor  4408  sotric  4800  sotrieq  4801  isso2i  4806  soxp  6920  unxpwdom2  8112  cflim2  8700  cfpwsdom  9016  ltapr  9477  ltxrlt  9711  isprm4  14633  euclemma  14664  islpi  20163  restntr  20196  alexsubALTlem2  21061  alexsubALTlem3  21062  2bornot2b  25899  disjorf  28191  funcnv5mpt  28274  ballotlemodife  29338  3orit  30355  dfon2lem5  30440  ecase13d  30974  elicc3  30978  nn0prpw  30984  onsucuni3  31734  orfa  32279  unitresl  32282  cnf1dd  32290  tsim1  32336  ifpidg  36105  ifpim123g  36114  ifpororb  36119  ifpor123g  36122  dfxor4  36328  df3or2  36330  frege83  36512  dffrege99  36528  frege131  36560  frege133  36562  pm10.541  36686  xrssre  37525  elprn2  37654  iundjiun  38206  r19.32  38459