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

Metamath Proof Explorer

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 ) )