Theorem spc3egv

Description: Existential specialization with three quantifiers, using implicit substitution. (Contributed by NM, 12-May-2008) Avoid ax-10 and ax-11 . (Revised by Gino Giotto, 20-Aug-2023) (Proof shortened by Wolf Lammen, 25-Aug-2023)

	Ref	Expression
Hypothesis	spc3egv.1	|- ( ( x = A /\ y = B /\ z = C ) -> ( ph <-> ps ) )
Assertion	spc3egv	|- ( ( A e. V /\ B e. W /\ C e. X ) -> ( ps -> E. x E. y E. z ph ) )

Proof

Step	Hyp	Ref	Expression
1		spc3egv.1	|- ( ( x = A /\ y = B /\ z = C ) -> ( ph <-> ps ) )
2		elex	|- ( A e. V -> A e. _V )
3		elex	|- ( B e. W -> B e. _V )
4		elex	|- ( C e. X -> C e. _V )
5		simp1	|- ( ( A e. _V /\ B e. _V /\ C e. _V ) -> A e. _V )
6	1	3coml	|- ( ( y = B /\ z = C /\ x = A ) -> ( ph <-> ps ) )
7	6	3expa	|- ( ( ( y = B /\ z = C ) /\ x = A ) -> ( ph <-> ps ) )
8	7	pm5.74da	|- ( ( y = B /\ z = C ) -> ( ( x = A -> ph ) <-> ( x = A -> ps ) ) )
9	8	spc2egv	|- ( ( B e. _V /\ C e. _V ) -> ( ( x = A -> ps ) -> E. y E. z ( x = A -> ph ) ) )
10		19.37v	|- ( E. z ( x = A -> ph ) <-> ( x = A -> E. z ph ) )
11	10	exbii	|- ( E. y E. z ( x = A -> ph ) <-> E. y ( x = A -> E. z ph ) )
12		19.37v	|- ( E. y ( x = A -> E. z ph ) <-> ( x = A -> E. y E. z ph ) )
13	11 12	bitri	|- ( E. y E. z ( x = A -> ph ) <-> ( x = A -> E. y E. z ph ) )
14	9 13	syl6ib	|- ( ( B e. _V /\ C e. _V ) -> ( ( x = A -> ps ) -> ( x = A -> E. y E. z ph ) ) )
15	14	pm2.86d	|- ( ( B e. _V /\ C e. _V ) -> ( x = A -> ( ps -> E. y E. z ph ) ) )
16	15	3adant1	|- ( ( A e. _V /\ B e. _V /\ C e. _V ) -> ( x = A -> ( ps -> E. y E. z ph ) ) )
17	16	imp	|- ( ( ( A e. _V /\ B e. _V /\ C e. _V ) /\ x = A ) -> ( ps -> E. y E. z ph ) )
18	5 17	spcimedv	|- ( ( A e. _V /\ B e. _V /\ C e. _V ) -> ( ps -> E. x E. y E. z ph ) )
19	2 3 4 18	syl3an	|- ( ( A e. V /\ B e. W /\ C e. X ) -> ( ps -> E. x E. y E. z ph ) )