Theorem 3comr 1235

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

Syntax hints:   -> wi 4   /\ w3a 1002

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 1004

This theorem is referenced by:  nnacan  6658  le2tri3i  8255  ltaddsublt  8718  div12ap  8841  lemul12b  9008  zdivadd  9536  zdivmul  9537  elfz  10210  fzmmmeqm  10254  fzrev  10280  absdiflt  11603  absdifle  11604  dvds0lem  12312  dvdsmulc  12330  dvds2add  12336  dvds2sub  12337  dvdstr  12339  lcmdvds  12601  psmettri2  15002  xmettri2  15035