3anrabdioph

Description: Diophantine set builder for ternary conjunctions. (Contributed by Stefan O'Rear, 10-Oct-2014)

		Ref	Expression
	Assertion	3anrabdioph	$⊢ (\{t \in ({ℕ_{0}}^{(1 \dots N)}) \| φ\} \in Dioph (N) \land \{t \in ({ℕ_{0}}^{(1 \dots N)}) \| ψ\} \in Dioph (N) \land \{t \in ({ℕ_{0}}^{(1 \dots N)}) \| χ\} \in Dioph (N)) \to \{t \in ({ℕ_{0}}^{(1 \dots N)}) \| (φ \land ψ \land χ)\} \in Dioph (N)$

Step	Hyp	Ref	Expression
1		df-3an	$⊢ (φ \land ψ \land χ) \leftrightarrow ((φ \land ψ) \land χ)$
2	1	rabbii	$⊢ \{t \in ({ℕ_{0}}^{(1 \dots N)}) \| (φ \land ψ \land χ)\} = \{t \in ({ℕ_{0}}^{(1 \dots N)}) \| ((φ \land ψ) \land χ)\}$
3		anrabdioph	$⊢ (\{t \in ({ℕ_{0}}^{(1 \dots N)}) \| φ\} \in Dioph (N) \land \{t \in ({ℕ_{0}}^{(1 \dots N)}) \| ψ\} \in Dioph (N)) \to \{t \in ({ℕ_{0}}^{(1 \dots N)}) \| (φ \land ψ)\} \in Dioph (N)$
4		anrabdioph	$⊢ (\{t \in ({ℕ_{0}}^{(1 \dots N)}) \| (φ \land ψ)\} \in Dioph (N) \land \{t \in ({ℕ_{0}}^{(1 \dots N)}) \| χ\} \in Dioph (N)) \to \{t \in ({ℕ_{0}}^{(1 \dots N)}) \| ((φ \land ψ) \land χ)\} \in Dioph (N)$
5	3 4	sylan	$⊢ ((\{t \in ({ℕ_{0}}^{(1 \dots N)}) \| φ\} \in Dioph (N) \land \{t \in ({ℕ_{0}}^{(1 \dots N)}) \| ψ\} \in Dioph (N)) \land \{t \in ({ℕ_{0}}^{(1 \dots N)}) \| χ\} \in Dioph (N)) \to \{t \in ({ℕ_{0}}^{(1 \dots N)}) \| ((φ \land ψ) \land χ)\} \in Dioph (N)$
6	2 5	eqeltrid	$⊢ ((\{t \in ({ℕ_{0}}^{(1 \dots N)}) \| φ\} \in Dioph (N) \land \{t \in ({ℕ_{0}}^{(1 \dots N)}) \| ψ\} \in Dioph (N)) \land \{t \in ({ℕ_{0}}^{(1 \dots N)}) \| χ\} \in Dioph (N)) \to \{t \in ({ℕ_{0}}^{(1 \dots N)}) \| (φ \land ψ \land χ)\} \in Dioph (N)$
7	6	3impa	$⊢ (\{t \in ({ℕ_{0}}^{(1 \dots N)}) \| φ\} \in Dioph (N) \land \{t \in ({ℕ_{0}}^{(1 \dots N)}) \| ψ\} \in Dioph (N) \land \{t \in ({ℕ_{0}}^{(1 \dots N)}) \| χ\} \in Dioph (N)) \to \{t \in ({ℕ_{0}}^{(1 \dots N)}) \| (φ \land ψ \land χ)\} \in Dioph (N)$

Metamath Proof Explorer