Theorem
exa1
Add an antecedent in an existentially quantified formula. (Contributed by BJ, 6-Oct-2018.)
Conclusion
\( \vdash \exists x \, \varphi \rightarrow \exists x \, (\psi \rightarrow \varphi) \)
Proof
ax-1
eximi
_
This is the content in the right pane.