Metamath Proof Explorer


Theorem an42

Description: Rearrangement of 4 conjuncts. (Contributed by NM, 7-Feb-1996)

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

Proof

Step Hyp Ref Expression
1 an4
 |-  ( ( ( ph /\ ps ) /\ ( ch /\ th ) ) <-> ( ( ph /\ ch ) /\ ( ps /\ th ) ) )
2 ancom
 |-  ( ( ps /\ th ) <-> ( th /\ ps ) )
3 2 anbi2i
 |-  ( ( ( ph /\ ch ) /\ ( ps /\ th ) ) <-> ( ( ph /\ ch ) /\ ( th /\ ps ) ) )
4 1 3 bitri
 |-  ( ( ( ph /\ ps ) /\ ( ch /\ th ) ) <-> ( ( ph /\ ch ) /\ ( th /\ ps ) ) )