Definition df-or 359

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) (see ex-or in set.mm). After we define the constant true T. (df-tru 1319) and the constant false F. (df-fal 1320), we will be able to prove these truth table values: (( T. \/ T. ) <-> T. ) (truortru 1340), (( T. \/ F. ) <-> T. ) (truorfal 1341), (( F. \/ T. ) <-> T. ) (falortru 1342), and (( F. \/ F. ) <-> F. ) (falorfal 1343).

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 227. This is the justification for the definition, along with the fact that it introduces a new symbol \/. Contrast with /\ (df-an 360), -> (wi 4), -/\ (df-nan 1288), and \/_ (df-xor 1305) . (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 357	. 2 wff (ph \/ ps)
4	1	wn 3	. . 3 wff -. ph
5	4, 2	wi 4	. 2 wff (-. ph -> ps)
6	3, 5	wb 176	1 wff ((ph \/ ps) <-> (-. ph -> ps))

This definition is referenced by:  pm4.64  361  pm2.53  362  pm2.54  363  ori  364  orri  365  ord  366  imor  401  mtord  641  orbi2d  682  orimdi  820  ordi  834  pm5.17  858  pm5.6  878  orbidi  898  cador  1391  cadan  1392  19.30  1604  19.43  1605  nfor  1836  19.32  1875  dfsb3  2056  sbor  2066  axi12  2333  neor  2601  r19.30  2757  r19.32v  2758  r19.43  2767  dfif2  3665  ltfintrilem1  4466  evenodddisjlem1  4516  fce  6189