Description: Commutation in consequent. Swap 1st and 2nd. (Contributed by Jeff Hankins, 17-Nov-2009)
Ref | Expression | ||
---|---|---|---|
Hypothesis | 3com12d.1 | |- ( ph -> ( ps /\ ch /\ th ) ) |
|
Assertion | 3com12d | |- ( ph -> ( ch /\ ps /\ th ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3com12d.1 | |- ( ph -> ( ps /\ ch /\ th ) ) |
|
2 | id | |- ( ( ch /\ ps /\ th ) -> ( ch /\ ps /\ th ) ) |
|
3 | 2 | 3com12 | |- ( ( ps /\ ch /\ th ) -> ( ch /\ ps /\ th ) ) |
4 | 1 3 | syl | |- ( ph -> ( ch /\ ps /\ th ) ) |