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 559  ordi 598  orbi2d 616  pm5.17 670  pm5.6 690  biorf 737  hbor 1010  19.30 1087  19.32 1088  dfsb3 1228  sbor 1237  neor 1641  r19.32v 1761  undif4 2329  dfif2 2367  sotric 2866  so 2870  dfwe2 2941  wereu 2951  ordtri1 2986  ordtri3 2989  sdomdomtr 4475  ltapr 5163  islpi 7746  grothprim 8778  2bornot2b 8780

Copyright terms: Public domain