Theorem 3coml 1212

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

Syntax hints:   -> wi 4   /\ w3a 980

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 982

This theorem is referenced by:  3comr  1213  nndir  6545  f1oen2g  6811  f1dom2g  6812  ordiso  7097  addassnqg  7444  ltbtwnnqq  7477  nnanq0  7520  ltasrg  7832  recexgt0sr  7835  axmulass  7935  adddir  8012  axltadd  8091  ltleletr  8103  letr  8104  pnpcan2  8261  subdir  8407  div13ap  8714  zdiv  9408  xrletr  9877  fzen  10112  fzrevral2  10175  fzshftral  10177  fzind2  10309  mulbinom2  10730  elicc4abs  11241  dvdsnegb  11954  muldvds1  11962  muldvds2  11963  dvdscmul  11964  dvdsmulc  11965  dvdsgcd  12152  mulgcdr  12158  lcmgcdeq  12224  congr  12241  mulgnnass  13230  mettri  14552  cnmet  14709  addcncntoplem  14740