MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3com12 Unicode version

Theorem 3com12 1200
Description: Commutation in antecedent. Swap 1st and 3rd. (Contributed by NM, 28-Jan-1996.) (Proof shortened by Andrew Salmon, 13-May-2011.)
Hypothesis
Ref Expression
3exp.1
Assertion
Ref Expression
3com12

Proof of Theorem 3com12
StepHypRef Expression
1 3ancoma 980 . 2
2 3exp.1 . 2
31, 2sylbi 195 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\w3a 973
This theorem is referenced by:  3adant2l  1222  3adant2r  1223  brelrng  5237  fresaunres1  5763  fvun2  5945  onfununi  7031  oaword  7217  nnaword  7295  nnmword  7301  ecopovtrn  7433  fpmg  7464  tskord  9179  ltadd2  9709  mul12  9767  add12  9814  addsub  9854  addsubeq4  9858  ppncan  9884  leadd1  10045  ltaddsub2  10052  leaddsub2  10054  ltsub1  10073  ltsub2  10074  div23  10251  ltmul1  10417  ltmulgt11  10427  lediv1  10432  ledivmulOLD  10444  lemuldiv  10449  ltdiv2  10455  zdiv  10958  xltadd1  11477  xltmul1  11513  iooneg  11669  icoshft  11671  fzaddel  11747  fzshftral  11795  facwordi  12367  swrdspsleq  12673  abssubge0  13160  climshftlem  13397  znnenlem  13945  dvdsmul1  14005  divalglem8  14058  divalgb  14062  pcfac  14418  mhmmulg  16174  xrsdsreval  18463  cnmptcom  20179  hmeof1o2  20264  ordthmeo  20303  cxplt2  23079  axcontlem8  24274  clwwlkndivn  24837  vcdi  25445  isvci  25475  dipdi  25758  dipsubdi  25764  hvadd12  25952  hvmulcom  25960  his5  26003  bcs3  26100  chj12  26452  spansnmul  26482  homul12  26724  hoaddsub  26735  lnopmul  26886  lnopaddmuli  26892  lnopsubmuli  26894  lnfnaddmuli  26964  leop2  27043  dmdsl3  27234  chirredlem3  27311  atmd2  27319  cdj3lem3  27357  signstfvc  28531  cnambfre  30063  3com12d  30128  sdclem2  30235  lcmgcdeq  31216  addrcom  31384  stoweidlem17  31799  sigaras  32072  sigarms  32073  3imp21  33341  uun123p1  33606  sineq0ALT  33737
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
  Copyright terms: Public domain W3C validator