Theorem
animorlr
Conjunction implies disjunction with one common formula (3/4). (Contributed by BJ, 4-Oct-2019.)
Conclusion
\( \vdash \varphi \wedge \psi \rightarrow \chi \vee \varphi \)
Proof
simpl
olcd
_
This is the content in the right pane.