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  6790  le2tri3i  8441  ltaddsublt  8907  div12ap  9032  lemul12b  9199  zdivadd  9745  zdivmul  9746  elfz  10433  fzmmmeqm  10480  fzrev  10507  absdiflt  11880  absdifle  11881  dvds0lem  12592  dvdsmulc  12610  dvds2add  12616  dvds2sub  12617  dvdstr  12619  lcmdvds  12881  psmettri2  15571  xmettri2  15604