This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem rspc3ev

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

Ref Expression
Hypotheses rspc3v.1 ⊢ x = A → φ ↔ χ
rspc3v.2 ⊢ y = B → χ ↔ θ
rspc3v.3 ⊢ z = C → θ ↔ ψ
Assertion rspc3ev ⊢ A ∈ R ∧ B ∈ S ∧ C ∈ T ∧ ψ → ∃ x ∈ R ∃ y ∈ S ∃ z ∈ T φ

Proof

Step Hyp Ref Expression
1 rspc3v.1 ⊢ x = A → φ ↔ χ
2 rspc3v.2 ⊢ y = B → χ ↔ θ
3 rspc3v.3 ⊢ z = C → θ ↔ ψ
4 simpl1 ⊢ A ∈ R ∧ B ∈ S ∧ C ∈ T ∧ ψ → A ∈ R
5 simpl2 ⊢ A ∈ R ∧ B ∈ S ∧ C ∈ T ∧ ψ → B ∈ S
6 3 rspcev ⊢ C ∈ T ∧ ψ → ∃ z ∈ T θ
7 6 3ad2antl3 ⊢ A ∈ R ∧ B ∈ S ∧ C ∈ T ∧ ψ → ∃ z ∈ T θ
8 1 rexbidv ⊢ x = A → ∃ z ∈ T φ ↔ ∃ z ∈ T χ
9 2 rexbidv ⊢ y = B → ∃ z ∈ T χ ↔ ∃ z ∈ T θ
10 8 9 rspc2ev ⊢ A ∈ R ∧ B ∈ S ∧ ∃ z ∈ T θ → ∃ x ∈ R ∃ y ∈ S ∃ z ∈ T φ
11 4 5 7 10 syl3anc ⊢ A ∈ R ∧ B ∈ S ∧ C ∈ T ∧ ψ → ∃ x ∈ R ∃ y ∈ S ∃ z ∈ T φ