Definition df-or 360

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 21682). After we define the constant true T. (df-tru 1325) and the constant false F. (df-fal 1326), we will be able to prove these truth table values: ( ( T. \/ T. ) <-> T. ) (truortru 1346), ( ( T. \/ F. ) <-> T. ) (truorfal 1347), ( ( F. \/ T. ) <-> T. ) (falortru 1348), and ( ( F. \/ F. ) <-> F. ) (falorfal 1349).

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 228. This is the justification for the definition, along with the fact that it introduces a new symbol \/. Contrast with /\ (df-an 361), -> (wi 4), -/\ (df-nan 1294), and \/_ (df-xor 1311) . (Contributed by NM, 5-Aug-1993.)

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 358	. 2 wff ( ph \/ ps )
4	1	wn 3	. . 3 wff -. ph
5	4, 2	wi 4	. 2 wff ( -. ph -> ps )
6	3, 5	wb 177	1 wff ( ( ph \/ ps ) <-> ( -. ph -> ps ) )

This definition is referenced by:  pm4.64  362  pm2.53  363  pm2.54  364  ori  365  orri  366  ord  367  imor  402  mtord  642  orbi2d  683  orimdi  821  ordi  835  pm5.17  859  pm5.6  879  orbidi  899  cador  1397  cadan  1398  19.30  1611  19.43  1612  nfor  1854  19.32  1892  dfsb3  2105  sbor  2115  neor  2651  r19.30  2813  r19.32v  2814  r19.43  2823  dfif2  3701  disjor  4156  sotric  4489  sotrieq  4490  isso2i  4495  soxp  6418  unxpwdom2  7512  cflim2  8099  cfpwsdom  8415  ltapr  8878  ltxrlt  9102  isprm4  13044  euclemma  13063  islpi  17167  restntr  17200  alexsubALTlem2  18032  alexsubALTlem3  18033  2bornot2b  21711  disjorf  23974  funcnv5mpt  24037  ballotlemodife  24708  3orit  25122  dfon2lem5  25357  ecase13d  26206  elicc3  26210  nn0prpw  26216  pm10.541  27430  r19.32  27812  sborNEW7  29270  dfsb3NEW7  29340