Metamath Proof Explorer

Theorem 3an6

Description: Analogue of an4 for triple conjunction. (Contributed by Scott Fenton, 16-Mar-2011) (Proof shortened by Andrew Salmon, 25-May-2011)

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

Step	Hyp	Ref	Expression
1		an6	\|- ( ( ( ph /\ ch /\ ta ) /\ ( ps /\ th /\ et ) ) <-> ( ( ph /\ ps ) /\ ( ch /\ th ) /\ ( ta /\ et ) ) )
2	1	bicomi	\|- ( ( ( ph /\ ps ) /\ ( ch /\ th ) /\ ( ta /\ et ) ) <-> ( ( ph /\ ch /\ ta ) /\ ( ps /\ th /\ et ) ) )

Step

Hyp

Ref

Expression

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

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