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 25716). 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 1465), ( ( T. \/ F. ) <-> T. ) (truorfal 1466), ( ( F. \/ T. ) <-> T. ) (falortru 1467), and ( ( F. \/ F. ) <-> F. ) (falorfal 1468).

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  1506  19.43  1740  19.32v  1781  nfor  1993  19.32  2024  dfsb3  2169  sbor  2193  neor  2755  r19.30  2980  r19.32v  2981  r19.43  2991  dfif2  3917  disjor  4411  sotric  4801  sotrieq  4802  isso2i  4807  soxp  6920  unxpwdom2  8103  cflim2  8691  cfpwsdom  9007  ltapr  9469  ltxrlt  9703  isprm4  14605  euclemma  14636  islpi  20096  restntr  20129  alexsubALTlem2  20994  alexsubALTlem3  20995  2bornot2b  25746  disjorf  28028  funcnv5mpt  28112  ballotlemodife  29156  3orit  30135  dfon2lem5  30220  ecase13d  30754  elicc3  30758  nn0prpw  30764  orfa  32019  unitresl  32022  cnf1dd  32030  tsim1  32076  ifpidg  35834  ifpim123g  35843  ifpororb  35848  ifpor123g  35851  dfxor4  35997  frege83  36179  dffrege99  36195  frege131  36227  frege133  36229  pm10.541  36353  elprn2  37286  iundjiun  37807  r19.32  37979