Theorem 3comr 1189

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

Syntax hints:   -> wi 4   /\ w3a 962

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

This theorem depends on definitions:  df-bi 116  df-3an 964

This theorem is referenced by:  nnacan  6401  le2tri3i  7865  ltaddsublt  8326  div12ap  8447  lemul12b  8612  zdivadd  9133  zdivmul  9134  elfz  9789  fzmmmeqm  9831  fzrev  9857  absdiflt  10857  absdifle  10858  dvds0lem  11492  dvdsmulc  11510  dvds2add  11516  dvds2sub  11517  dvdstr  11519  lcmdvds  11749  psmettri2  12486  xmettri2  12519