rexlimdvvva

Description: Inference from Theorem 19.23 of Margaris p. 90, for three restricted quantifiers. (Contributed by AV, 23-Aug-2025)

		Ref	Expression
	Hypothesis	rexlimdvvva.1	$⊢ (φ \land (x \in A \land y \in B \land z \in C)) \to (ψ \to χ)$
	Assertion	rexlimdvvva	$⊢ φ \to (\exists x \in A \exists y \in B \exists z \in C ψ \to χ)$

Step	Hyp	Ref	Expression
1		rexlimdvvva.1	$⊢ (φ \land (x \in A \land y \in B \land z \in C)) \to (ψ \to χ)$
2		df-3an	$⊢ (x \in A \land y \in B \land z \in C) \leftrightarrow ((x \in A \land y \in B) \land z \in C)$
3	1	ex	$⊢ φ \to ((x \in A \land y \in B \land z \in C) \to (ψ \to χ))$
4	2 3	biimtrrid	$⊢ φ \to (((x \in A \land y \in B) \land z \in C) \to (ψ \to χ))$
5	4	expdimp	$⊢ (φ \land (x \in A \land y \in B)) \to (z \in C \to (ψ \to χ))$
6	5	rexlimdv	$⊢ (φ \land (x \in A \land y \in B)) \to (\exists z \in C ψ \to χ)$
7	6	rexlimdvva	$⊢ φ \to (\exists x \in A \exists y \in B \exists z \in C ψ \to χ)$

Metamath Proof Explorer