Metamath Proof Explorer


Theorem 3com12d

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 ) )

Proof

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 ) )