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  6785  le2tri3i  8436  ltaddsublt  8902  div12ap  9027  lemul12b  9194  zdivadd  9740  zdivmul  9741  elfz  10428  fzmmmeqm  10475  fzrev  10502  absdiflt  11875  absdifle  11876  dvds0lem  12587  dvdsmulc  12605  dvds2add  12611  dvds2sub  12612  dvdstr  12614  lcmdvds  12876  psmettri2  15520  xmettri2  15553