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 (¬ φ → ψ) for (φ ⋁ ψ), 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	⊢ ((φ ⋁ ψ) ↔ (¬ φ → ψ))

Detailed syntax breakdown of Definition df-or

Step	Hyp	Ref	Expression
1		wph	. . 3 wff φ
2		wps	. . 3 wff ψ
3	1, 2	wo 222	. 2 wff (φ ⋁ ψ)
4	1	wn 2	. . 3 wff ¬ φ
5	4, 2	wi 3	. 2 wff (¬ φ → ψ)
6	3, 5	wb 146	1 wff ((φ ⋁ ψ) ↔ (¬ φ → ψ))

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 666  pm5.6 686  biorf 733  hbor 1005  19.30 1081  19.32 1082  dfsb3 1221  sbor 1230  neor 1630  r19.32v 1750  undif4 2315  dfif2 2353  sotric 2851  so 2855  dfwe2 2925  wereu 2935  ordtri1 2970  ordtri3 2973  sdomdomtr 4449  ltapr 5123  islpi 7690  grothprim 8722  2bornot2b 8724

Copyright terms: Public domain