Theorem 3comr 1214

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

Syntax hints:   -> wi 4   /\ w3a 981

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 983

This theorem is referenced by:  nnacan  6621  le2tri3i  8216  ltaddsublt  8679  div12ap  8802  lemul12b  8969  zdivadd  9497  zdivmul  9498  elfz  10171  fzmmmeqm  10215  fzrev  10241  absdiflt  11518  absdifle  11519  dvds0lem  12227  dvdsmulc  12245  dvds2add  12251  dvds2sub  12252  dvdstr  12254  lcmdvds  12516  psmettri2  14915  xmettri2  14948