Theorem an6 902

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 777	. . . 4 |- ((ph /\ ps /\ ch) <-> ((ph /\ ps) /\ ch))
2		df-3an 777	. . . 4 |- ((th /\ ta /\ et) <-> ((th /\ ta) /\ et))
3	1, 2	anbi12i 482	. . 3 |- (((ph /\ ps /\ ch) /\ (th /\ ta /\ et)) <-> (((ph /\ ps) /\ ch) /\ ((th /\ ta) /\ et)))
4		an4 506	. . 3 |- ((((ph /\ ps) /\ ch) /\ ((th /\ ta) /\ et)) <-> (((ph /\ ps) /\ (th /\ ta)) /\ (ch /\ et)))
5		an4 506	. . . 4 |- (((ph /\ ps) /\ (th /\ ta)) <-> ((ph /\ th) /\ (ps /\ ta)))
6	5	anbi1i 481	. . 3 |- ((((ph /\ ps) /\ (th /\ ta)) /\ (ch /\ et)) <-> (((ph /\ th) /\ (ps /\ ta)) /\ (ch /\ et)))
7	3, 4, 6	3bitr 177	. 2 |- (((ph /\ ps /\ ch) /\ (th /\ ta /\ et)) <-> (((ph /\ th) /\ (ps /\ ta)) /\ (ch /\ et)))
8		df-3an 777	. 2 |- (((ph /\ th) /\ (ps /\ ta) /\ (ch /\ et)) <-> (((ph /\ th) /\ (ps /\ ta)) /\ (ch /\ et)))
9	7, 8	bitr4 176	1 |- (((ph /\ ps /\ ch) /\ (th /\ ta /\ et)) <-> ((ph /\ th) /\ (ps /\ ta) /\ (ch /\ et)))

Syntax hints:   <-> wb 146   /\ wa 223   /\ w3a 775

This theorem is referenced by:  abfii4OLD 4564  distrlem3pr 5129  ltdiv2t 5887  elfzuzb 6476  efcltlem1 7304  subbasOLD 7644  iscau3 7938  iscau4 7940  infi1 10447  infi1OLD 10448  ficli 10472  ficliOLD 10473  filintf 10569  infi 10578  infiOLD 10579  rcfpfillem4 10591  rcfpfillem4OLD 10592

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 147  df-an 225  df-3an 777

Copyright terms: Public domain