Theorem 3comr 1211

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

Syntax hints:   -> wi 4   /\ w3a 978

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

This theorem depends on definitions:  df-bi 117  df-3an 980

This theorem is referenced by:  nnacan  6515  le2tri3i  8068  ltaddsublt  8530  div12ap  8653  lemul12b  8820  zdivadd  9344  zdivmul  9345  elfz  10016  fzmmmeqm  10060  fzrev  10086  absdiflt  11103  absdifle  11104  dvds0lem  11810  dvdsmulc  11828  dvds2add  11834  dvds2sub  11835  dvdstr  11837  lcmdvds  12081  psmettri2  13913  xmettri2  13946