Theorem hbanOLD

Obsolete version of hban as of 22-Oct-2026. (Contributed by NM, 14-May-1993.) (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 \)
Conclusion
\( \vdash \varphi \wedge \psi \rightarrow \forall x \, (\varphi \wedge \psi) \)
Proof
hbOLD.1
l1
nf5i _
hbOLD.2
nf5i _
nfan l1 _
nf5ri _