Theorem eeeeanv 15233

Description: Rearrange existential quantifiers.

Assertion

Ref	Expression
eeeeanv	|- (E.wE.xE.yE.z((ph /\ ps /\ ch) /\ th) <-> ((E.wph /\ E.xps /\ E.ych) /\ E.zth))

Distinct variable groups:   ch,w,x,z   ph,x,y   ph,z   ps,w,y   ps,z   th,w,x,y

Proof of Theorem eeeeanv

Step	Hyp	Ref	Expression
1		19.41vvv 1984	. . . . 5 |- (E.xE.yE.z((ps /\ ch /\ th) /\ ph) <-> (E.xE.yE.z(ps /\ ch /\ th) /\ ph))
2		ancom 510	. . . . 5 |- ((E.xE.yE.z(ps /\ ch /\ th) /\ ph) <-> (ph /\ E.xE.yE.z(ps /\ ch /\ th)))
3		eeeanv 2004	. . . . . 6 |- (E.xE.yE.z(ps /\ ch /\ th) <-> (E.xps /\ E.ych /\ E.zth))
4	3	anbi2i 804	. . . . 5 |- ((ph /\ E.xE.yE.z(ps /\ ch /\ th)) <-> (ph /\ (E.xps /\ E.ych /\ E.zth)))
5	1, 2, 4	3bitri 334	. . . 4 |- (E.xE.yE.z((ps /\ ch /\ th) /\ ph) <-> (ph /\ (E.xps /\ E.ych /\ E.zth)))
6	5	exbii 1716	. . 3 |- (E.wE.xE.yE.z((ps /\ ch /\ th) /\ ph) <-> E.w(ph /\ (E.xps /\ E.ych /\ E.zth)))
7		19.41v 1982	. . 3 |- (E.w(ph /\ (E.xps /\ E.ych /\ E.zth)) <-> (E.wph /\ (E.xps /\ E.ych /\ E.zth)))
8	6, 7	bitri 306	. 2 |- (E.wE.xE.yE.z((ps /\ ch /\ th) /\ ph) <-> (E.wph /\ (E.xps /\ E.ych /\ E.zth)))
9		ancom 510	. . . . 5 |- (((ps /\ ch /\ th) /\ ph) <-> (ph /\ (ps /\ ch /\ th)))
10		and4com 15228	. . . . 5 |- ((ph /\ (ps /\ ch /\ th)) <-> ((ph /\ ps /\ ch) /\ th))
11	9, 10	bitri 306	. . . 4 |- (((ps /\ ch /\ th) /\ ph) <-> ((ph /\ ps /\ ch) /\ th))
12	11	3exbii 1718	. . 3 |- (E.xE.yE.z((ps /\ ch /\ th) /\ ph) <-> E.xE.yE.z((ph /\ ps /\ ch) /\ th))
13	12	exbii 1716	. 2 |- (E.wE.xE.yE.z((ps /\ ch /\ th) /\ ph) <-> E.wE.xE.yE.z((ph /\ ps /\ ch) /\ th))
14		and4com 15228	. 2 |- ((E.wph /\ (E.xps /\ E.ych /\ E.zth)) <-> ((E.wph /\ E.xps /\ E.ych) /\ E.zth))
15	8, 13, 14	3bitr3i 338	1 |- (E.wE.xE.yE.z((ph /\ ps /\ ch) /\ th) <-> ((E.wph /\ E.xps /\ E.ych) /\ E.zth))

Syntax hints:   <-> wb 231   /\ wa 433   /\ w3a 1130  E.wex 1644

This theorem is referenced by:  elo 15311

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1621  ax-gen 1622  ax-17 1634  ax-4 1637  ax-5o 1639  ax-6o 1642

This theorem depends on definitions:  df-bi 232  df-an 435  df-3an 1132  df-ex 1645

Copyright terms: Public domain