Theorem hb3an

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

Hypotheses
hb.1
\( \vdash \varphi \rightarrow \forall x \, \varphi \)
hb.2
\( \vdash \psi \rightarrow \forall x \, \psi \)
hb.3
\( \vdash \chi \rightarrow \forall x \, \chi \)
Conclusion
\( \vdash \varphi \wedge \psi \wedge \chi \rightarrow \forall x \, (\varphi \wedge \psi \wedge \chi) \)
Proof
l0
df-3an
\( \vdash \varphi \wedge \psi \wedge \chi \leftrightarrow \varphi \wedge \psi \wedge \chi \)
l1
hb.1
hb.2
l3
hban l1 _
hb.3
hban l3 _
\( \vdash \varphi \wedge \psi \wedge \chi \rightarrow \forall x \, (\varphi \wedge \psi \wedge \chi) \)
hbxfrbi l0 _