Theorem an6

Description: Rearrangement of 6 conjuncts. (Contributed by NM, 13-Mar-1995)

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

Proof

Step	Hyp	Ref	Expression
1		an4	|- ( ( ( ( ph /\ ps ) /\ ch ) /\ ( ( th /\ ta ) /\ et ) ) <-> ( ( ( ph /\ ps ) /\ ( th /\ ta ) ) /\ ( ch /\ et ) ) )
2		an4	|- ( ( ( ph /\ ps ) /\ ( th /\ ta ) ) <-> ( ( ph /\ th ) /\ ( ps /\ ta ) ) )
3	1 2	bianbi	|- ( ( ( ( ph /\ ps ) /\ ch ) /\ ( ( th /\ ta ) /\ et ) ) <-> ( ( ( ph /\ th ) /\ ( ps /\ ta ) ) /\ ( ch /\ et ) ) )
4		df-3an	|- ( ( ph /\ ps /\ ch ) <-> ( ( ph /\ ps ) /\ ch ) )
5		df-3an	|- ( ( th /\ ta /\ et ) <-> ( ( th /\ ta ) /\ et ) )
6	4 5	anbi12i	|- ( ( ( ph /\ ps /\ ch ) /\ ( th /\ ta /\ et ) ) <-> ( ( ( ph /\ ps ) /\ ch ) /\ ( ( th /\ ta ) /\ et ) ) )
7		df-3an	|- ( ( ( ph /\ th ) /\ ( ps /\ ta ) /\ ( ch /\ et ) ) <-> ( ( ( ph /\ th ) /\ ( ps /\ ta ) ) /\ ( ch /\ et ) ) )
8	3 6 7	3bitr4i	|- ( ( ( ph /\ ps /\ ch ) /\ ( th /\ ta /\ et ) ) <-> ( ( ph /\ th ) /\ ( ps /\ ta ) /\ ( ch /\ et ) ) )