Theorem 3comr 1242

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

This proof depends on syntax axioms:   -> wi 4   /\ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  nnacan  6785  le2tri3i  8435  ltaddsublt  8901  div12ap  9026  lemul12b  9193  zdivadd  9739  zdivmul  9740  elfz  10427  fzmmmeqm  10474  fzrev  10501  absdiflt  11873  absdifle  11874  dvds0lem  12584  dvdsmulc  12602  dvds2add  12608  dvds2sub  12609  dvdstr  12611  lcmdvds  12873  psmettri2  15478  xmettri2  15511