rspc3ev

Description: 3-variable restricted existential specialization, using implicit substitution. (Contributed by NM, 25-Jul-2012)

	Ref	Expression
Hypotheses	rspc3v.1	$⊢ x = A \to (φ \leftrightarrow χ)$
	rspc3v.2	$⊢ y = B \to (χ \leftrightarrow θ)$
	rspc3v.3	$⊢ z = C \to (θ \leftrightarrow ψ)$
Assertion	rspc3ev	$⊢ ((A \in R \land B \in S \land C \in T) \land ψ) \to \exists x \in R \exists y \in S \exists z \in T φ$

Step	Hyp	Ref	Expression
1		rspc3v.1	$⊢ x = A \to (φ \leftrightarrow χ)$
2		rspc3v.2	$⊢ y = B \to (χ \leftrightarrow θ)$
3		rspc3v.3	$⊢ z = C \to (θ \leftrightarrow ψ)$
4		simpl1	$⊢ ((A \in R \land B \in S \land C \in T) \land ψ) \to A \in R$
5		simpl2	$⊢ ((A \in R \land B \in S \land C \in T) \land ψ) \to B \in S$
6	3	rspcev	$⊢ (C \in T \land ψ) \to \exists z \in T θ$
7	6	3ad2antl3	$⊢ ((A \in R \land B \in S \land C \in T) \land ψ) \to \exists z \in T θ$
8	1	rexbidv	$⊢ x = A \to (\exists z \in T φ \leftrightarrow \exists z \in T χ)$
9	2	rexbidv	$⊢ y = B \to (\exists z \in T χ \leftrightarrow \exists z \in T θ)$
10	8 9	rspc2ev	$⊢ (A \in R \land B \in S \land \exists z \in T θ) \to \exists x \in R \exists y \in S \exists z \in T φ$
11	4 5 7 10	syl3anc	$⊢ ((A \in R \land B \in S \land C \in T) \land ψ) \to \exists x \in R \exists y \in S \exists z \in T φ$

Metamath Proof Explorer