Theorem eeeeanv 10436

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 1307	. . . . 5 |- (E.xE.yE.z((ps /\ ch /\ th) /\ ph) <-> (E.xE.yE.z(ps /\ ch /\ th) /\ ph))
2		ancom 435	. . . . 5 |- ((E.xE.yE.z(ps /\ ch /\ th) /\ ph) <-> (ph /\ E.xE.yE.z(ps /\ ch /\ th)))
3		eeeanv 1324	. . . . . 6 |- (E.xE.yE.z(ps /\ ch /\ th) <-> (E.xps /\ E.ych /\ E.zth))
4	3	anbi2i 480	. . . . 5 |- ((ph /\ E.xE.yE.z(ps /\ ch /\ th)) <-> (ph /\ (E.xps /\ E.ych /\ E.zth)))
5	1, 2, 4	3bitr 177	. . . 4 |- (E.xE.yE.z((ps /\ ch /\ th) /\ ph) <-> (ph /\ (E.xps /\ E.ych /\ E.zth)))
6	5	exbii 1051	. . 3 |- (E.wE.xE.yE.z((ps /\ ch /\ th) /\ ph) <-> E.w(ph /\ (E.xps /\ E.ych /\ E.zth)))
7		19.41v 1305	. . 3 |- (E.w(ph /\ (E.xps /\ E.ych /\ E.zth)) <-> (E.wph /\ (E.xps /\ E.ych /\ E.zth)))
8	6, 7	bitr 173	. 2 |- (E.wE.xE.yE.z((ps /\ ch /\ th) /\ ph) <-> (E.wph /\ (E.xps /\ E.ych /\ E.zth)))
9		ancom 435	. . . . 5 |- (((ps /\ ch /\ th) /\ ph) <-> (ph /\ (ps /\ ch /\ th)))
10		and4com 10433	. . . . 5 |- ((ph /\ (ps /\ ch /\ th)) <-> ((ph /\ ps /\ ch) /\ th))
11	9, 10	bitr 173	. . . 4 |- (((ps /\ ch /\ th) /\ ph) <-> ((ph /\ ps /\ ch) /\ th))
12	11	3exbi 1053	. . 3 |- (E.xE.yE.z((ps /\ ch /\ th) /\ ph) <-> E.xE.yE.z((ph /\ ps /\ ch) /\ th))
13	12	exbii 1051	. 2 |- (E.wE.xE.yE.z((ps /\ ch /\ th) /\ ph) <-> E.wE.xE.yE.z((ph /\ ps /\ ch) /\ th))
14		and4com 10433	. 2 |- ((E.wph /\ (E.xps /\ E.ych /\ E.zth)) <-> ((E.wph /\ E.xps /\ E.ych) /\ E.zth))
15	8, 13, 14	3bitr3 181	1 |- (E.wE.xE.yE.z((ph /\ ps /\ ch) /\ th) <-> ((E.wph /\ E.xps /\ E.ych) /\ E.zth))

Syntax hints:   <-> wb 146   /\ wa 223   /\ w3a 775  E.wex 980

This theorem is referenced by:  elo 10444

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3an 777  df-ex 981

Copyright terms: Public domain