This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) ) )