Theorem bnj1276

Description: First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

	Ref	Expression
Hypotheses	bnj1276.1	$$⊢\phi \to \forall x\phi$$
	bnj1276.2	$$⊢\psi \to \forall x\psi$$
	bnj1276.3	$$⊢\chi \to \forall x\chi$$
	bnj1276.4	$$⊢\theta \leftrightarrow \left(\phi \wedge \psi \wedge \chi \right)$$
Assertion	bnj1276	$$⊢\theta \to \forall x\theta$$

Proof

Step	Hyp	Ref	Expression
1		bnj1276.1	$$⊢\phi \to \forall x\phi$$
2		bnj1276.2	$$⊢\psi \to \forall x\psi$$
3		bnj1276.3	$$⊢\chi \to \forall x\chi$$
4		bnj1276.4	$$⊢\theta \leftrightarrow \left(\phi \wedge \psi \wedge \chi \right)$$
5	1 2 3	hb3an	$$⊢\left(\phi \wedge \psi \wedge \chi \right)\to \forall x\left(\phi \wedge \psi \wedge \chi \right)$$
6	4 5	hbxfrbi	$$⊢\theta \to \forall x\theta$$