Theorem 3comr 1146

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

Syntax hints:   -> wi 4   /\ w3a 919

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

This theorem depends on definitions:  df-bi 115  df-3an 921

This theorem is referenced by:  nnacan  6108  le2tri3i  7219  ltaddsublt  7671  div12ap  7782  lemul12b  7939  zdivadd  8436  zdivmul  8437  elfz  9035  fzmmmeqm  9076  fzrev  9101  absdiflt  9978  absdifle  9979  dvds0lem  10205  dvdsmulc  10223  dvds2add  10229  dvds2sub  10230  dvdstr  10232  lcmdvds  10461