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  6666  le2tri3i  8266  ltaddsublt  8729  div12ap  8852  lemul12b  9019  zdivadd  9547  zdivmul  9548  elfz  10222  fzmmmeqm  10266  fzrev  10292  absdiflt  11619  absdifle  11620  dvds0lem  12328  dvdsmulc  12346  dvds2add  12352  dvds2sub  12353  dvdstr  12355  lcmdvds  12617  psmettri2  15018  xmettri2  15051