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  8434  ltaddsublt  8899  div12ap  9024  lemul12b  9191  zdivadd  9735  zdivmul  9736  elfz  10417  fzmmmeqm  10464  fzrev  10491  absdiflt  11858  absdifle  11859  dvds0lem  12568  dvdsmulc  12586  dvds2add  12592  dvds2sub  12593  dvdstr  12595  lcmdvds  12857  psmettri2  15429  xmettri2  15462