Description: Define disjunction (logical "or"). Definition of Margaris p. 49. When the left operand, right operand, or both are true, the result is true; when both sides are false, the result is false. For example, it is true that ( 2 = 3 \/ 4 = 4 ) ( ex-or ). After we define the constant true T. ( df-tru ) and the constant false F. ( df-fal ), we will be able to prove these truth table values: ( ( T. \/ T. ) <-> T. ) ( truortru ), ( ( T. \/ F. ) <-> T. ) ( truorfal ), ( ( F. \/ T. ) <-> T. ) ( falortru ), and ( ( F. \/ F. ) <-> F. ) ( falorfal ).
Contrast with /\ ( df-an ), -> ( wi ), -/\ ( df-nan ), and \/_ ( df-xor ). (Contributed by NM, 27-Dec-1992)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | df-or | |- ( ( ph \/ ps ) <-> ( -. ph -> ps ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | wph | |- ph |
|
| 1 | wps | |- ps |
|
| 2 | 0 1 | wo | |- ( ph \/ ps ) |
| 3 | 0 | wn | |- -. ph |
| 4 | 3 1 | wi | |- ( -. ph -> ps ) |
| 5 | 2 4 | wb | |- ( ( ph \/ ps ) <-> ( -. ph -> ps ) ) |