Theorem 3an4ancom24

Description: Commutative law for a conjunction with a triple conjunction: second and forth positions interchanged. (Contributed by AV, 18-Feb-2022)

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

Proof

Step	Hyp	Ref	Expression
1		an4com24	|- ( ( ( ph /\ ps ) /\ ( ch /\ th ) ) <-> ( ( ph /\ th ) /\ ( ch /\ ps ) ) )
2		3an4anass	|- ( ( ( ph /\ ps /\ ch ) /\ th ) <-> ( ( ph /\ ps ) /\ ( ch /\ th ) ) )
3		3an4anass	|- ( ( ( ph /\ th /\ ch ) /\ ps ) <-> ( ( ph /\ th ) /\ ( ch /\ ps ) ) )
4	1 2 3	3bitr4i	|- ( ( ( ph /\ ps /\ ch ) /\ th ) <-> ( ( ph /\ th /\ ch ) /\ ps ) )