Theorem
anabsi6
Absorption of antecedent into conjunction. (Contributed by NM, 14-Aug-2000.)
Hypothesis
anabsi6.1
\( \vdash \varphi \rightarrow \psi \wedge \varphi \rightarrow \chi \)
Conclusion
\( \vdash \varphi \wedge \psi \rightarrow \chi \)
Proof
anabsi6.1
ancomsd
_
anabsi5
_
This is the content in the right pane.