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 ( 2 = 3 \/ 4 = 4 ) (ex-or 24807). After we define the constant true T. (df-tru 1377) and the constant false F. (df-fal 1380), we will be able to prove these truth table values: ( ( T. \/ T. ) <-> T. ) (truortru 1402), ( ( T. \/ F. ) <-> T. ) (truorfal 1403), ( ( F. \/ T. ) <-> T. ) (falortru 1404), and ( ( F. \/ F. ) <-> F. ) (falorfal 1405).

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 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 1339), and \/_ (df-xor 1356) . (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 368	. 2 wff ( ph \/ ps )
4	1	wn 3	. . 3 wff -. ph
5	4, 2	wi 4	. 2 wff ( -. ph -> ps )
6	3, 5	wb 184	1 wff ( ( ph \/ ps ) <-> ( -. ph -> ps ) )

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  844  ordi  860  pm5.17  884  pm5.6  905  orbidi  925  cador  1437  cadanOLD  1439  19.43  1665  nfor  1877  19.32  1911  dfsb3  2083  sbor  2108  neor  2786  r19.30  3001  r19.32v  3002  r19.43  3012  dfif2  3936  disjor  4426  sotric  4821  sotrieq  4822  isso2i  4827  soxp  6888  unxpwdom2  8005  cflim2  8634  cfpwsdom  8950  ltapr  9414  ltxrlt  9646  fzocatel  11839  isprm4  14077  euclemma  14099  islpi  19411  restntr  19444  alexsubALTlem2  20278  alexsubALTlem3  20279  2bornot2b  24836  disjorf  27101  funcnv5mpt  27171  ballotlemodife  28064  sgn3da  28108  3orit  28555  dfon2lem5  28784  ecase13d  29697  elicc3  29701  nn0prpw  29707  orfa  30071  unitresl  30074  cnf1dd  30082  tsim1  30130  tsbi3  30135  pm10.541  30807  elunnel1  30949  elunnel2  30950  elprn1  31132  elprn2  31133  fourierdlem70  31434  fourierdlem80  31444  fourierdlem93  31457  r19.32  31596