Inference rule 57: Conjunction elimination (declared)
(a) Given that the conjunction \phi \wedge \psi holds, we may infer that \phi holds: \cfrac{\vdash (\phi \wedge \psi)}{\vdash \phi}. (b) Given that \phi \wedge \psi holds, we may infer that \psi holds: \cfrac{\vdash (\phi \wedge \psi)}{\vdash \psi}.