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 555  ordi 594  orbi2d 612  pm5.17 665  pm5.6 685  biorf 732  hbor 984  19.30 1061  19.32 1062  dfsb3 1210  sbor 1219  neor 1614  r19.32v 1734  undif4 2296  dfif2 2334  sotric 2824  so 2828  dfwe2 2898  wereu 2908  ordtri1 2943  ordtri3 2946  sdomdomtr 4403  ltapr 5074  islpi 7638  grothprim 8635  2bornot2b 8965

Copyright terms: Public domain