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 | ⊢ ( ( 𝜑 ∨ 𝜓 ) ↔ ( ¬ 𝜑 → 𝜓 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | wph | ⊢ 𝜑 | |
| 1 | wps | ⊢ 𝜓 | |
| 2 | 0 1 | wo | ⊢ ( 𝜑 ∨ 𝜓 ) |
| 3 | 0 | wn | ⊢ ¬ 𝜑 |
| 4 | 3 1 | wi | ⊢ ( ¬ 𝜑 → 𝜓 ) |
| 5 | 2 4 | wb | ⊢ ( ( 𝜑 ∨ 𝜓 ) ↔ ( ¬ 𝜑 → 𝜓 ) ) |