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	2	anbi1i	|- ( ( ( ( ph /\ ps ) /\ ( th /\ ta ) ) /\ ( ch /\ et ) ) <-> ( ( ( ph /\ th ) /\ ( ps /\ ta ) ) /\ ( ch /\ et ) ) )
4	1 3	bitri	|- ( ( ( ( ph /\ ps ) /\ ch ) /\ ( ( th /\ ta ) /\ et ) ) <-> ( ( ( ph /\ th ) /\ ( ps /\ ta ) ) /\ ( ch /\ et ) ) )
5		df-3an	|- ( ( ph /\ ps /\ ch ) <-> ( ( ph /\ ps ) /\ ch ) )
6		df-3an	|- ( ( th /\ ta /\ et ) <-> ( ( th /\ ta ) /\ et ) )
7	5 6	anbi12i	|- ( ( ( ph /\ ps /\ ch ) /\ ( th /\ ta /\ et ) ) <-> ( ( ( ph /\ ps ) /\ ch ) /\ ( ( th /\ ta ) /\ et ) ) )
8		df-3an	|- ( ( ( ph /\ th ) /\ ( ps /\ ta ) /\ ( ch /\ et ) ) <-> ( ( ( ph /\ th ) /\ ( ps /\ ta ) ) /\ ( ch /\ et ) ) )
9	4 7 8	3bitr4i	|- ( ( ( ph /\ ps /\ ch ) /\ ( th /\ ta /\ et ) ) <-> ( ( ph /\ th ) /\ ( ps /\ ta ) /\ ( ch /\ et ) ) )