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  6600  le2tri3i  8183  ltaddsublt  8646  div12ap  8769  lemul12b  8936  zdivadd  9464  zdivmul  9465  elfz  10138  fzmmmeqm  10182  fzrev  10208  absdiflt  11436  absdifle  11437  dvds0lem  12145  dvdsmulc  12163  dvds2add  12169  dvds2sub  12170  dvdstr  12172  lcmdvds  12434  psmettri2  14833  xmettri2  14866