Theorem 3comr 1201

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 1200	. 2 |- ( ( ps /\ ch /\ ph ) -> th )
3	2	3coml 1200	1 |- ( ( ch /\ ph /\ ps ) -> th )

Syntax hints:   -> wi 4   /\ w3a 968

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 970

This theorem is referenced by:  nnacan  6480  le2tri3i  8007  ltaddsublt  8469  div12ap  8590  lemul12b  8756  zdivadd  9280  zdivmul  9281  elfz  9950  fzmmmeqm  9993  fzrev  10019  absdiflt  11034  absdifle  11035  dvds0lem  11741  dvdsmulc  11759  dvds2add  11765  dvds2sub  11766  dvdstr  11768  lcmdvds  12011  psmettri2  12968  xmettri2  13001