df-or

Definition.

Arguments:

phi (pr), psi (pr),

Assertions:

((phiveepsi)leftrightarrow(lnotphitopsi))