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 556  ordi 595  orbi2d 613  pm5.17 667  pm5.6 687  biorf 734  hbor 1007  19.30 1084  19.32 1085  dfsb3 1225  sbor 1234  neor 1636  r19.32v 1756  undif4 2322  dfif2 2360  sotric 2856  so 2860  dfwe2 2931  wereu 2941  ordtri1 2976  ordtri3 2979  sdomdomtr 4458  ltapr 5134  islpi 7709  grothprim 8738  2bornot2b 8740

Copyright terms: Public domain