Definition df-or 368

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 25263). After we define the constant true T. (df-tru 1402) and the constant false F. (df-fal 1405), we will be able to prove these truth table values: ( ( T. \/ T. ) <-> T. ) (truortru 1427), ( ( T. \/ F. ) <-> T. ) (truorfal 1428), ( ( F. \/ T. ) <-> T. ) (falortru 1429), and ( ( F. \/ F. ) <-> F. ) (falorfal 1430).

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 369), -> (wi 4), -/\ (df-nan 1342), and \/_ (df-xor 1363) . (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 366	. 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  370  pm2.53  371  pm2.54  372  ori  373  orri  374  ord  375  imor  410  mtord  658  orbi2d  699  orimdi  845  ordi  862  pm5.17  886  pm5.6  910  orbidi  930  nanbi  1350  nanbiOLD  1351  cador  1465  19.43  1701  19.32v  1738  nfor  1943  19.32  1975  dfsb3  2119  sbor  2143  neor  2706  r19.30  2927  r19.32v  2928  r19.43  2938  dfif2  3859  disjor  4352  sotric  4740  sotrieq  4741  isso2i  4746  soxp  6812  unxpwdom2  7929  cflim2  8556  cfpwsdom  8872  ltapr  9334  ltxrlt  9566  isprm4  14229  euclemma  14251  islpi  19736  restntr  19769  alexsubALTlem2  20633  alexsubALTlem3  20634  2bornot2b  25293  disjorf  27569  funcnv5mpt  27657  ballotlemodife  28619  3orit  29258  dfon2lem5  29384  ecase13d  30297  elicc3  30301  nn0prpw  30307  orfa  30645  unitresl  30648  cnf1dd  30656  tsim1  30703  pm10.541  31440  elprn2  31806  r19.32  32338  ifpim123g  38119  ifpidg  38121  ifpor123g  38148  ifpororb  38149  dfxor4  38259  frege83  38445  dffrege99  38461  frege131  38493  frege133  38495