Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Steven Nguyen
Utility theorems
3rspcedvd
Next ⟩
rabdif
Metamath Proof Explorer
Ascii
Unicode
Theorem
3rspcedvd
Description:
Triple application of
rspcedvd
.
(Contributed by
Steven Nguyen
, 27-Feb-2023)
Ref
Expression
Hypotheses
3rspcedvd.a
⊢
φ
→
A
∈
D
3rspcedvd.b
⊢
φ
→
B
∈
D
3rspcedvd.c
⊢
φ
→
C
∈
D
3rspcedvd.1
⊢
φ
∧
x
=
A
→
ψ
↔
χ
3rspcedvd.2
⊢
φ
∧
y
=
B
→
χ
↔
θ
3rspcedvd.3
⊢
φ
∧
z
=
C
→
θ
↔
τ
3rspcedvd.4
⊢
φ
→
τ
Assertion
3rspcedvd
⊢
φ
→
∃
x
∈
D
∃
y
∈
D
∃
z
∈
D
ψ
Proof
Step
Hyp
Ref
Expression
1
3rspcedvd.a
⊢
φ
→
A
∈
D
2
3rspcedvd.b
⊢
φ
→
B
∈
D
3
3rspcedvd.c
⊢
φ
→
C
∈
D
4
3rspcedvd.1
⊢
φ
∧
x
=
A
→
ψ
↔
χ
5
3rspcedvd.2
⊢
φ
∧
y
=
B
→
χ
↔
θ
6
3rspcedvd.3
⊢
φ
∧
z
=
C
→
θ
↔
τ
7
3rspcedvd.4
⊢
φ
→
τ
8
4
2rexbidv
⊢
φ
∧
x
=
A
→
∃
y
∈
D
∃
z
∈
D
ψ
↔
∃
y
∈
D
∃
z
∈
D
χ
9
5
rexbidv
⊢
φ
∧
y
=
B
→
∃
z
∈
D
χ
↔
∃
z
∈
D
θ
10
3
6
7
rspcedvd
⊢
φ
→
∃
z
∈
D
θ
11
2
9
10
rspcedvd
⊢
φ
→
∃
y
∈
D
∃
z
∈
D
χ
12
1
8
11
rspcedvd
⊢
φ
→
∃
x
∈
D
∃
y
∈
D
∃
z
∈
D
ψ