Description: Rearrangement of 4 conjuncts. (Contributed by Rodolfo Medina, 24-Sep-2010) (Proof shortened by Andrew Salmon, 29-Jun-2011)
Ref | Expression | ||
---|---|---|---|
Assertion | an43 | |- ( ( ( ph /\ ps ) /\ ( ch /\ th ) ) <-> ( ( ph /\ th ) /\ ( ps /\ ch ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | an42 | |- ( ( ( ph /\ th ) /\ ( ps /\ ch ) ) <-> ( ( ph /\ ps ) /\ ( ch /\ th ) ) ) |
|
2 | 1 | bicomi | |- ( ( ( ph /\ ps ) /\ ( ch /\ th ) ) <-> ( ( ph /\ th ) /\ ( ps /\ ch ) ) ) |