Definition df-or 224

Description: Define disjunction (logical 'or'). This is our first use of the biconditional connective in a definition; we use it 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 pm4.2 170. This is the justification for the definition, along with the fact that it introduces a new symbol \/. Definition of [Margaris] p. 49.

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

This definition is referenced by:  pm4.64 226  pm2.54 227  dfor2 229  ori 230  orri 231  ord 232  orrd 233  imor 234  oridm 243  orcom 246  orel1 251  orbi2i 255  or12 258  pm4.78 354  pm3.48 557  ordi 596  orbi2d 614  pm5.17 668  pm5.6 688  biorf 735  hbor 1008  19.30 1085  19.32 1086  dfsb3 1226  sbor 1235  neor 1638  r19.32v 1758  undif4 2325  dfif2 2363  sotric 2860  so 2864  dfwe2 2935  wereu 2945  ordtri1 2980  ordtri3 2983  sdomdomtr 4469  ltapr 5151  islpi 7749  grothprim 8783  2bornot2b 8785

Copyright terms: Public domain