bnj982

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

	Ref	Expression
Hypotheses	bnj982.1	$⊢ φ \to \forall x φ$
	bnj982.2	$⊢ ψ \to \forall x ψ$
	bnj982.3	$⊢ χ \to \forall x χ$
	bnj982.4	$⊢ θ \to \forall x θ$
Assertion	bnj982	$⊢ (φ \land ψ \land χ \land θ) \to \forall x (φ \land ψ \land χ \land θ)$

Step	Hyp	Ref	Expression
1		bnj982.1	$⊢ φ \to \forall x φ$
2		bnj982.2	$⊢ ψ \to \forall x ψ$
3		bnj982.3	$⊢ χ \to \forall x χ$
4		bnj982.4	$⊢ θ \to \forall x θ$
5		df-bnj17	$⊢ (φ \land ψ \land χ \land θ) \leftrightarrow ((φ \land ψ \land χ) \land θ)$
6	1 2 3	hb3an	$⊢ (φ \land ψ \land χ) \to \forall x (φ \land ψ \land χ)$
7	6 4	hban	$⊢ ((φ \land ψ \land χ) \land θ) \to \forall x ((φ \land ψ \land χ) \land θ)$
8	5 7	hbxfrbi	$⊢ (φ \land ψ \land χ \land θ) \to \forall x (φ \land ψ \land χ \land θ)$

Metamath Proof Explorer