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  6789  le2tri3i  8441  ltaddsublt  8907  div12ap  9032  lemul12b  9199  zdivadd  9746  zdivmul  9747  elfz  10434  fzmmmeqm  10481  fzrev  10508  absdiflt  11881  absdifle  11882  dvds0lem  12593  dvdsmulc  12611  dvds2add  12617  dvds2sub  12618  dvdstr  12620  lcmdvds  12882  psmettri2  15554  xmettri2  15587