Metamath Proof Explorer


Definition df-or

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 φ ψ ¬ φ ψ

Detailed syntax breakdown

Step Hyp Ref Expression
0 wph wff φ
1 wps wff ψ
2 0 1 wo wff φ ψ
3 0 wn wff ¬ φ
4 3 1 wi wff ¬ φ ψ
5 2 4 wb wff φ ψ ¬ φ ψ