Theorem 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	⊢ ( 𝜑 → ∀ 𝑥 𝜑 )
	bnj982.2	⊢ ( 𝜓 → ∀ 𝑥 𝜓 )
	bnj982.3	⊢ ( 𝜒 → ∀ 𝑥 𝜒 )
	bnj982.4	⊢ ( 𝜃 → ∀ 𝑥 𝜃 )
Assertion	bnj982	⊢ ( ( 𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃 ) → ∀ 𝑥 ( 𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃 ) )

Proof

Step	Hyp	Ref	Expression
1		bnj982.1	⊢ ( 𝜑 → ∀ 𝑥 𝜑 )
2		bnj982.2	⊢ ( 𝜓 → ∀ 𝑥 𝜓 )
3		bnj982.3	⊢ ( 𝜒 → ∀ 𝑥 𝜒 )
4		bnj982.4	⊢ ( 𝜃 → ∀ 𝑥 𝜃 )
5		df-bnj17	⊢ ( ( 𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃 ) ↔ ( ( 𝜑 ∧ 𝜓 ∧ 𝜒 ) ∧ 𝜃 ) )
6	1 2 3	hb3an	⊢ ( ( 𝜑 ∧ 𝜓 ∧ 𝜒 ) → ∀ 𝑥 ( 𝜑 ∧ 𝜓 ∧ 𝜒 ) )
7	6 4	hban	⊢ ( ( ( 𝜑 ∧ 𝜓 ∧ 𝜒 ) ∧ 𝜃 ) → ∀ 𝑥 ( ( 𝜑 ∧ 𝜓 ∧ 𝜒 ) ∧ 𝜃 ) )
8	5 7	hbxfrbi	⊢ ( ( 𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃 ) → ∀ 𝑥 ( 𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃 ) )