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