Theorem 3coml 1203

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

Hypothesis

Ref	Expression
3exp.1

Assertion

Ref	Expression
3coml

Proof of Theorem 3coml

Step	Hyp	Ref	Expression
1		3exp.1	. . 3
2	1	3com23 1202	. 2
3	2	3com13 1201	1

Syntax hints:  ->wi 4  /\w3a 973

This theorem is referenced by:  3comr  1204  omwordri  7240  oeword  7258  f1oen2g  7552  f1dom2g  7553  ordiso  7962  en3lplem2  8053  axdc3lem4  8854  ltasr  9498  adddir  9608  axltadd  9679  pnpcan2  9882  subdir  10016  ltaddsub  10051  leaddsub  10053  mulcan2g  10228  div13  10253  ltdiv2  10455  lediv2  10460  zdiv  10958  xadddir  11517  xadddi2r  11519  fzen  11732  fzrevral2  11793  fzshftral  11795  ssfzoulel  11906  fzind2  11924  flflp1  11944  digit1  12300  faclbnd5  12376  ccatlcan  12697  elicc4abs  13152  dvdsnegb  14001  muldvds1  14008  muldvds2  14009  dvdscmul  14010  dvdsmulc  14011  dvdscmulr  14012  dvdsmulcr  14013  dvdsgcd  14181  mulgcdr  14186  coprmdvds  14243  mulgnnass  16170  gaass  16335  elfm3  20451  mettri  20855  cnmet  21279  addcnlem  21368  bcthlem5  21767  isppw2  23389  vmappw  23390  bcmono  23552  colinearalg  24213  ax5seglem1  24231  ax5seglem2  24232  vcdir  25446  vcass  25447  imsmetlem  25596  hvaddcan2  25988  hvsubcan2  25992  ltflcei  30043  fzmul  30233  rabrenfdioph  30748  lcmgcdeq  31216  uun123p2  33607  isosctrlem1ALT  33734  pclfinclN  35674

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 185  df-an 371  df-3an 975