Theorem hban

If \( x \) is not free in \( \varphi \) and \( \psi \), it is not free in \( \varphi \wedge \psi \). (Contributed by NM, 14-May-1993.) (Proof shortened by Wolf Lammen, 2-Jan-2018.) Reduce axiom dependencies. (Revised by SN and Sky Winter, 22-Oct-2026.)

Hypotheses
hb.1
\( \vdash \varphi \rightarrow \forall x \, \varphi \)
hb.2
\( \vdash \psi \rightarrow \forall x \, \psi \)
Conclusion
\( \vdash \varphi \wedge \psi \rightarrow \forall x \, (\varphi \wedge \psi) \)
Proof
l0
hb.1
l1
hb.2
pm3.2
alrimdh l0 l1 _
imp _