Theorem 3comr 1151

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

Syntax hints:   -> wi 4   /\ w3a 924

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106

This theorem depends on definitions:  df-bi 115  df-3an 926

This theorem is referenced by:  nnacan  6271  le2tri3i  7593  ltaddsublt  8048  div12ap  8161  lemul12b  8322  zdivadd  8835  zdivmul  8836  elfz  9430  fzmmmeqm  9472  fzrev  9498  absdiflt  10525  absdifle  10526  dvds0lem  11084  dvdsmulc  11102  dvds2add  11108  dvds2sub  11109  dvdstr  11111  lcmdvds  11339