Description: A rearrangement of conjuncts. (Contributed by Rodolfo Medina, 25-Sep-2010)
Ref | Expression | ||
---|---|---|---|
Assertion | an3 | |- ( ( ( ph /\ ps ) /\ ( ch /\ th ) ) -> ( ph /\ th ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | an43 | |- ( ( ( ph /\ ps ) /\ ( ch /\ th ) ) <-> ( ( ph /\ th ) /\ ( ps /\ ch ) ) ) |
|
2 | 1 | simplbi | |- ( ( ( ph /\ ps ) /\ ( ch /\ th ) ) -> ( ph /\ th ) ) |