Definition df-or 241

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

This definition is referenced by:  pm4.64 243  pm2.54 244  dfor2 246  ori 247  orri 248  ord 249  orrd 250  imor 251  oridm 262  oridmOLD 263  orcom 266  orel1 271  orbi2i 275  or12 278  ioran 331  pm4.78 381  pm3.48 616  ordiOLD 657  orbi2d 676  pm5.17 731  pm5.6 752  biorf 807  hbor 1355  19.30 1436  19.30OLD 1437  19.32 1438  dfsb3 1596  sbor 1605  neor 2096  r19.32v 2230  r19.43 2238  undif4OLD 2931  dfif2 2984  sotric 3615  sotrieq 3616  so 3620  wereu 3654  ordtri1OLD 3694  ordtri3OLD 3698  dfwe2OLD 3862  sdomdomtr 5532  ltapr 6303  islpi 9025  grothprim 10141  2bornot2b 10143  bnj28 12391  prmdvdsmul 13784  3orit 13811  r19.30 13817  dffr5 13831  dfon2lem5 13853  soxp 13950  nxtor 14312  mtord 15346  ecase13d 15350  elicc3 15362  subntr 15425  alexsublem2 15438  alexsublem3 15439  alexsublem4 15440  locfincomp 15514  isufil2 15565  ufprim 15569  fimax2g 15769  pm10.541 16314

Copyright terms: Public domain