Definition df-or 434

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

This definition is referenced by:  pm4.64 436  pm2.54 437  ori 439  orri 440  ord 441  pm2.62 443  dfor2OLD 446  imor 449  pm2.53 466  orel1OLD 468  ioran 520  oridmOLD 559  orcomOLD 563  orbi2iOLD 573  or12OLD 580  pm4.78OLD 652  orbi2d 812  pm3.48OLD 951  orimdi 964  pm5.17 1027  pm5.17OLD 1028  pm5.6 1054  biorfOLD 1070  orbidi 1083  hbor 1673  19.30 1751  19.32 1752  dfsb3 1901  sbor 1910  neor 2375  r19.30 2507  r19.32v 2508  r19.43 2516  dfif2 3214  sotric 3806  sotrieq 3807  so 3810  wereu 3840  soxp 5253  sdomdomtr 5741  fimax2g 5893  cflim2 6350  cfpwsdom 6528  ltapr 6746  isprm4 9507  euclemma 9515  islpi 10041  grothprim 11170  2bornot2b 11172  bnj28 13348  3orit 14688  r19.30OLD 14694  dfon2lem5 14734  soxpOLD 14850  nxtor 15281  mtord 16431  ecase13d 16435  elicc3 16447  subntr 16510  alexsublem2 16523  alexsublem3 16524  alexsublem4 16525  locfincomp 16599  isufil2 16650  ufprim 16654  fimax2gOLD 16854  pm10.541 17399

Copyright terms: Public domain