Theorem hb3anOLD

Obsolete version of hb3an as of 23-Oct-2026. (Contributed by NM, 14-Sep-2003.) (Proof shortened by Wolf Lammen, 2-Jan-2018.) (Proof modification is discouraged.) (New usage is discouraged.)

Hypotheses
hbOLD.1
\( \vdash \varphi \rightarrow \forall x \, \varphi \)
hbOLD.2
\( \vdash \psi \rightarrow \forall x \, \psi \)
hbOLD.3
\( \vdash \chi \rightarrow \forall x \, \chi \)
Conclusion
\( \vdash \varphi \wedge \psi \wedge \chi \rightarrow \forall x \, (\varphi \wedge \psi \wedge \chi) \)
Proof
hbOLD.1
l1
nf5i _
hbOLD.2
l3
nf5i _
hbOLD.3
nf5i _
nf3an l1 l3 _
nf5ri _