Theorem eeeanv

Description: Distribute three existential quantifiers over a conjunction. (Contributed by NM, 26-Jul-1995) (Proof shortened by Andrew Salmon, 25-May-2011) Reduce distinct variable restrictions. (Revised by Wolf Lammen, 20-Jan-2018)

	Ref	Expression
Assertion	eeeanv	|- ( E. x E. y E. z ( ph /\ ps /\ ch ) <-> ( E. x ph /\ E. y ps /\ E. z ch ) )

Proof

Step	Hyp	Ref	Expression
1		eeanv	|- ( E. x E. y ( ph /\ ps ) <-> ( E. x ph /\ E. y ps ) )
2	1	anbi1i	|- ( ( E. x E. y ( ph /\ ps ) /\ E. z ch ) <-> ( ( E. x ph /\ E. y ps ) /\ E. z ch ) )
3		df-3an	|- ( ( ph /\ ps /\ ch ) <-> ( ( ph /\ ps ) /\ ch ) )
4	3	exbii	|- ( E. z ( ph /\ ps /\ ch ) <-> E. z ( ( ph /\ ps ) /\ ch ) )
5		19.42v	|- ( E. z ( ( ph /\ ps ) /\ ch ) <-> ( ( ph /\ ps ) /\ E. z ch ) )
6	4 5	bitri	|- ( E. z ( ph /\ ps /\ ch ) <-> ( ( ph /\ ps ) /\ E. z ch ) )
7	6	2exbii	|- ( E. x E. y E. z ( ph /\ ps /\ ch ) <-> E. x E. y ( ( ph /\ ps ) /\ E. z ch ) )
8		nfv	|- F/ y ch
9	8	nfex	|- F/ y E. z ch
10	9	19.41	|- ( E. y ( ( ph /\ ps ) /\ E. z ch ) <-> ( E. y ( ph /\ ps ) /\ E. z ch ) )
11	10	exbii	|- ( E. x E. y ( ( ph /\ ps ) /\ E. z ch ) <-> E. x ( E. y ( ph /\ ps ) /\ E. z ch ) )
12		nfv	|- F/ x ch
13	12	nfex	|- F/ x E. z ch
14	13	19.41	|- ( E. x ( E. y ( ph /\ ps ) /\ E. z ch ) <-> ( E. x E. y ( ph /\ ps ) /\ E. z ch ) )
15	7 11 14	3bitri	|- ( E. x E. y E. z ( ph /\ ps /\ ch ) <-> ( E. x E. y ( ph /\ ps ) /\ E. z ch ) )
16		df-3an	|- ( ( E. x ph /\ E. y ps /\ E. z ch ) <-> ( ( E. x ph /\ E. y ps ) /\ E. z ch ) )
17	2 15 16	3bitr4i	|- ( E. x E. y E. z ( ph /\ ps /\ ch ) <-> ( E. x ph /\ E. y ps /\ E. z ch ) )