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 25120). After we define the constant true T. (df-tru 1386) and the constant false F. (df-fal 1389), we will be able to prove these truth table values: ( ( T. \/ T. ) <-> T. ) (truortru 1411), ( ( T. \/ F. ) <-> T. ) (truorfal 1412), ( ( F. \/ T. ) <-> T. ) (falortru 1413), and ( ( F. \/ F. ) <-> F. ) (falorfal 1414).

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 1345), and \/_ (df-xor 1365) . (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  847  ordi  864  pm5.17  888  pm5.6  912  orbidi  932  nanbi  1353  cador  1446  19.43  1680  19.32v  1717  nfor  1921  19.32  1953  dfsb3  2101  sbor  2125  neor  2767  r19.30  2988  r19.32v  2989  r19.43  2999  dfif2  3928  disjor  4421  sotric  4816  sotrieq  4817  isso2i  4822  soxp  6898  unxpwdom2  8017  cflim2  8646  cfpwsdom  8962  ltapr  9426  ltxrlt  9658  isprm4  14209  euclemma  14231  islpi  19628  restntr  19661  alexsubALTlem2  20526  alexsubALTlem3  20527  2bornot2b  25150  disjorf  27418  funcnv5mpt  27489  ballotlemodife  28414  3orit  29070  dfon2lem5  29195  ecase13d  30107  elicc3  30111  nn0prpw  30117  orfa  30455  unitresl  30458  cnf1dd  30466  tsim1  30513  pm10.541  31226  elprn2  31594  r19.32  32126