Proposition 79: Commutativity of disjunction (inference rule)

Given that the disjunction (\phi \vee \psi) holds, we may infer that (\psi \vee \phi) holds: \cfrac{\vdash (\phi \vee \psi)}{\vdash (\psi \vee \phi)}.

Proof: First, assume \phi . Then, by disjunction introduction, \psi \vee \phi holds. But then we have showed that \phi entails \psi \vee \phi .

Next, assume that \psi holds. By disjunction introduction, we infer \psi \vee \phi holds. Hence, \psi entails \psi \vee \phi .

But our original premise was that \phi \vee \psi holds. By disjunction elimination, we conclude \psi \vee \phi holds. \square