# 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 ${⊢}\left({\phi }\vee {\psi }\right)↔\left(¬{\phi }\to {\psi }\right)$

### Detailed syntax breakdown

Step Hyp Ref Expression
0 wph ${wff}{\phi }$
1 wps ${wff}{\psi }$
2 0 1 wo ${wff}\left({\phi }\vee {\psi }\right)$
3 0 wn ${wff}¬{\phi }$
4 3 1 wi ${wff}\left(¬{\phi }\to {\psi }\right)$
5 2 4 wb ${wff}\left(\left({\phi }\vee {\psi }\right)↔\left(¬{\phi }\to {\psi }\right)\right)$