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