Theorem an6 1177

Description: Rearrangement of 6 conjuncts.

Assertion

Ref	Expression
an6	|- (((ph /\ ps /\ ch) /\ (th /\ ta /\ et)) <-> ((ph /\ th) /\ (ps /\ ta) /\ (ch /\ et)))

Proof of Theorem an6

Step	Hyp	Ref	Expression
1		df-3an 860	. . . 4 |- ((ph /\ ps /\ ch) <-> ((ph /\ ps) /\ ch))
2		df-3an 860	. . . 4 |- ((th /\ ta /\ et) <-> ((th /\ ta) /\ et))
3	1, 2	anbi12i 540	. . 3 |- (((ph /\ ps /\ ch) /\ (th /\ ta /\ et)) <-> (((ph /\ ps) /\ ch) /\ ((th /\ ta) /\ et)))
4		an4 564	. . 3 |- ((((ph /\ ps) /\ ch) /\ ((th /\ ta) /\ et)) <-> (((ph /\ ps) /\ (th /\ ta)) /\ (ch /\ et)))
5		an4 564	. . . 4 |- (((ph /\ ps) /\ (th /\ ta)) <-> ((ph /\ th) /\ (ps /\ ta)))
6	5	anbi1i 539	. . 3 |- ((((ph /\ ps) /\ (th /\ ta)) /\ (ch /\ et)) <-> (((ph /\ th) /\ (ps /\ ta)) /\ (ch /\ et)))
7	3, 4, 6	3bitri 194	. 2 |- (((ph /\ ps /\ ch) /\ (th /\ ta /\ et)) <-> (((ph /\ th) /\ (ps /\ ta)) /\ (ch /\ et)))
8		df-3an 860	. 2 |- (((ph /\ th) /\ (ps /\ ta) /\ (ch /\ et)) <-> (((ph /\ th) /\ (ps /\ ta)) /\ (ch /\ et)))
9	7, 8	bitr4i 193	1 |- (((ph /\ ps /\ ch) /\ (th /\ ta /\ et)) <-> ((ph /\ th) /\ (ps /\ ta) /\ (ch /\ et)))

Syntax hints:   <-> wb 163   /\ wa 240   /\ w3a 858

This theorem is referenced by:  abfii4 5654  distrlem3pr 6281  ltdiv2 7070  elfzuzb 7646  efcltlem1 8566  subbas 8914  iscau3 9216  iscau4 9218  filintf 10274  infi 10280  3an6 13803  infi1 14343  ficli 14353  rcfpfillem4 14931  fzadd2 15791  fzsplit 15792  iimulcl 15874  pi1gp 16095  paddasslem9 17289  paddasslem10 17290

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 164  df-an 242  df-3an 860

Copyright terms: Public domain