Theorem 3comr 1189

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

Syntax hints:   -> wi 4   /\ w3a 962

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 964

This theorem is referenced by:  nnacan  6408  le2tri3i  7872  ltaddsublt  8333  div12ap  8454  lemul12b  8619  zdivadd  9140  zdivmul  9141  elfz  9796  fzmmmeqm  9838  fzrev  9864  absdiflt  10864  absdifle  10865  dvds0lem  11503  dvdsmulc  11521  dvds2add  11527  dvds2sub  11528  dvdstr  11530  lcmdvds  11760  psmettri2  12497  xmettri2  12530