Theorem 3coml 1210

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

Syntax hints:   -> wi 4   /\ w3a 978

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 980

This theorem is referenced by:  3comr  1211  nndir  6481  f1oen2g  6745  f1dom2g  6746  ordiso  7025  addassnqg  7356  ltbtwnnqq  7389  nnanq0  7432  ltasrg  7744  recexgt0sr  7747  axmulass  7847  adddir  7923  axltadd  8001  ltleletr  8013  letr  8014  pnpcan2  8171  subdir  8317  div13ap  8622  zdiv  9312  xrletr  9777  fzen  10011  fzrevral2  10074  fzshftral  10076  fzind2  10207  mulbinom2  10604  elicc4abs  11069  dvdsnegb  11781  muldvds1  11789  muldvds2  11790  dvdscmul  11791  dvdsmulc  11792  dvdsgcd  11978  mulgcdr  11984  lcmgcdeq  12048  congr  12065  mulgnnass  12876  mettri  13424  cnmet  13581  addcncntoplem  13602