Theorem 3comr 1207

Description: Commutation in antecedent. Rotate right. (Contributed by NM, 28-Jan-1996.)

Hypothesis

Ref	Expression
3exp.1	|- ( ( ph /\ ps /\ ch ) -> th )

Assertion

Ref	Expression
3comr	|- ( ( ch /\ ph /\ ps ) -> th )

Proof of Theorem 3comr

Step	Hyp	Ref	Expression
1		3exp.1	. . 3 |- ( ( ph /\ ps /\ ch ) -> th )
2	1	3coml 1206	. 2 |- ( ( ps /\ ch /\ ph ) -> th )
3	2	3coml 1206	1 |- ( ( ch /\ ph /\ ps ) -> th )

Syntax hints:   -> wi 4   /\ w3a 974

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116  df-3an 976

This theorem is referenced by:  nnacan  6495  le2tri3i  8032  ltaddsublt  8494  div12ap  8615  lemul12b  8781  zdivadd  9305  zdivmul  9306  elfz  9975  fzmmmeqm  10018  fzrev  10044  absdiflt  11060  absdifle  11061  dvds0lem  11767  dvdsmulc  11785  dvds2add  11791  dvds2sub  11792  dvdstr  11794  lcmdvds  12037  psmettri2  13207  xmettri2  13240