This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	$⊢ φ \to \forall x φ$
	bnj1276.2	$⊢ ψ \to \forall x ψ$
	bnj1276.3	$⊢ χ \to \forall x χ$
	bnj1276.4	$⊢ θ \leftrightarrow (φ \land ψ \land χ)$
Assertion	bnj1276	$⊢ θ \to \forall x θ$

Step	Hyp	Ref	Expression
1		bnj1276.1	$⊢ φ \to \forall x φ$
2		bnj1276.2	$⊢ ψ \to \forall x ψ$
3		bnj1276.3	$⊢ χ \to \forall x χ$
4		bnj1276.4	$⊢ θ \leftrightarrow (φ \land ψ \land χ)$
5	1 2 3	hb3an	$⊢ (φ \land ψ \land χ) \to \forall x (φ \land ψ \land χ)$
6	4 5	hbxfrbi	$⊢ θ \to \forall x θ$