Theorem 3coml 1237

Description: Commutation in antecedent. Rotate left. (Contributed by NM, 28-Jan-1996.)

Hypothesis

Ref	Expression
3exp.1	|- ( ( ph /\ ps /\ ch ) -> th )

Assertion

Ref	Expression
3coml	|- ( ( ps /\ ch /\ ph ) -> th )

Proof of Theorem 3coml

Step	Hyp	Ref	Expression
1		3exp.1	. . 3 |- ( ( ph /\ ps /\ ch ) -> th )
2	1	3com23 1236	. 2 |- ( ( ph /\ ch /\ ps ) -> th )
3	2	3com13 1235	1 |- ( ( ps /\ ch /\ ph ) -> th )

Syntax hints:   -> wi 4   /\ w3a 1005

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

This theorem depends on definitions:  df-bi 117  df-3an 1007

This theorem is referenced by:  3comr  1238  nndir  6701  f1oen2g  6971  f1dom2g  6972  ordiso  7295  addassnqg  7662  ltbtwnnqq  7695  nnanq0  7738  ltasrg  8050  recexgt0sr  8053  axmulass  8153  adddir  8230  axltadd  8308  ltleletr  8320  letr  8321  pnpcan2  8478  subdir  8624  div13ap  8932  zdiv  9629  xrletr  10104  fzen  10340  fzrevral2  10403  fzshftral  10405  fzind2  10548  mulbinom2  10981  ccatlcan  11365  elicc4abs  11734  dvdsnegb  12449  muldvds1  12457  muldvds2  12458  dvdscmul  12459  dvdsmulc  12460  dvdsgcd  12663  mulgcdr  12669  lcmgcdeq  12735  congr  12752  mulgnnass  13824  mettri  15184  cnmet  15341  addcncntoplem  15372