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

Metamath Proof Explorer

Theorem 3rspcedvd

Description: Triple application of rspcedvd . (Contributed by Steven Nguyen, 27-Feb-2023)

Ref Expression
Hypotheses 3rspcedvd.a 
|- ( ph -> A e. D )
3rspcedvd.b 
|- ( ph -> B e. D )
3rspcedvd.c 
|- ( ph -> C e. D )
3rspcedvd.1 
|- ( ( ph /\ x = A ) -> ( ps <-> ch ) )
3rspcedvd.2 
|- ( ( ph /\ y = B ) -> ( ch <-> th ) )
3rspcedvd.3 
|- ( ( ph /\ z = C ) -> ( th <-> ta ) )
3rspcedvd.4 
|- ( ph -> ta )
Assertion 3rspcedvd 
|- ( ph -> E. x e. D E. y e. D E. z e. D ps )

Proof

Step Hyp Ref Expression
1 3rspcedvd.a 
 |-  ( ph -> A e. D )
2 3rspcedvd.b 
 |-  ( ph -> B e. D )
3 3rspcedvd.c 
 |-  ( ph -> C e. D )
4 3rspcedvd.1 
 |-  ( ( ph /\ x = A ) -> ( ps <-> ch ) )
5 3rspcedvd.2 
 |-  ( ( ph /\ y = B ) -> ( ch <-> th ) )
6 3rspcedvd.3 
 |-  ( ( ph /\ z = C ) -> ( th <-> ta ) )
7 3rspcedvd.4 
 |-  ( ph -> ta )
8 4 2rexbidv 
 |-  ( ( ph /\ x = A ) -> ( E. y e. D E. z e. D ps <-> E. y e. D E. z e. D ch ) )
9 5 rexbidv 
 |-  ( ( ph /\ y = B ) -> ( E. z e. D ch <-> E. z e. D th ) )
10 3 6 7 rspcedvd 
 |-  ( ph -> E. z e. D th )
11 2 9 10 rspcedvd 
 |-  ( ph -> E. y e. D E. z e. D ch )
12 1 8 11 rspcedvd 
 |-  ( ph -> E. x e. D E. y e. D E. z e. D ps )