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)\leftrightarrow \left(\neg \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\neg \phi$$
4	3 1	wi	$$wff\left(\neg \phi \to \psi \right)$$
5	2 4	wb	$$wff\left(\left(\phi \vee \psi \right)\leftrightarrow \left(\neg \phi \to \psi \right)\right)$$