Theorem
ala1
Add an antecedent in a universally quantified formula. (Contributed by BJ, 6-Oct-2018.)
Conclusion
\( \vdash \forall x \, \varphi \rightarrow \forall x \, (\psi \rightarrow \varphi) \)
Proof
ax-1
alimi
_
This is the content in the right pane.