Theorem 3coml 1272

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

Syntax hints:   -> wi 4   /\ w3a 1037

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197  df-an 386  df-3an 1039

This theorem is referenced by:  3comr  1273  omwordri  7652  oeword  7670  f1oen2g  7972  f1dom2g  7973  ordiso  8421  en3lplem2  8512  axdc3lem4  9275  ltasr  9921  adddir  10031  axltadd  10111  pnpcan2  10321  subdir  10464  ltaddsub  10502  leaddsub  10504  mulcan2g  10681  div13  10706  ltdiv2  10909  lediv2  10913  zdiv  11447  xadddir  12126  xadddi2r  12128  fzen  12358  fzrevral2  12426  fzshftral  12428  ssfzoulel  12562  fzind2  12586  flflp1  12608  mulbinom2  12984  digit1  12998  faclbnd5  13085  ccatlcan  13472  relexpreld  13780  elicc4abs  14059  dvdsnegb  14999  muldvds1  15006  muldvds2  15007  dvdscmul  15008  dvdsmulc  15009  dvdscmulr  15010  dvdsmulcr  15011  dvdsgcd  15261  mulgcdr  15267  lcmgcdeq  15325  coprmdvdsOLD  15367  congr  15378  mulgnnass  17576  mulgnnassOLD  17577  gaass  17730  elfm3  21754  mettri  22157  cnmet  22575  addcnlem  22667  bcthlem5  23125  isppw2  24841  vmappw  24842  bcmono  25002  colinearalg  25790  ax5seglem1  25808  ax5seglem2  25809  vcdir  27421  vcass  27422  imsmetlem  27545  hvaddcan2  27928  hvsubcan2  27932  sletr  31883  dfgcd3  33170  isbasisrelowllem1  33203  ltflcei  33397  fzmul  33537  pclfinclN  35236  rabrenfdioph  37378  uun123p2  39037  isosctrlem1ALT  39170