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

Theorem an12 797
Description: Swap two conjuncts. Note that the first digit (1) in the label refers to the outer conjunct position, and the next digit (2) to the inner conjunct position. (Contributed by NM, 12-Mar-1995.)
Assertion
Ref Expression
an12

Proof of Theorem an12
StepHypRef Expression
1 ancom 450 . . 3
21anbi1i 695 . 2
3 anass 649 . 2
4 anass 649 . 2
52, 3, 43bitr3i 275 1
Colors of variables: wff setvar class
Syntax hints:  <->wb 184  /\wa 369
This theorem is referenced by:  an32  798  an13  799  an12s  801  an4  824  ceqsrexv  3233  rmoan  3298  2reuswap  3302  reuind  3303  sbccomlem  3406  elunirab  4261  axsep  4572  reuxfr2d  4675  opeliunxp  5056  elres  5314  resoprab  6398  elrnmpt2res  6416  ov6g  6440  opabex3d  6778  opabex3  6779  oeeu  7271  xpassen  7631  omxpenlem  7638  dfac5lem2  8526  ltexprlem4  9438  rexuz2  11161  wrdeqswrdlsw  12674  2clim  13395  divalglem10  14060  bitsmod  14086  isssc  15189  eldmcoa  15392  issubrg  17429  isbasis2g  19449  tgval2  19457  is1stc2  19943  elflim2  20465  i1fres  22112  dvdsflsumcom  23464  vmasum  23491  logfac2  23492  axcontlem2  24268  2reuswap2  27387  reuxfr3d  27388  1stpreima  27524  elima4  29209  nofulllem5  29466  elfuns  29565  brimg  29587  dfrdg4  29600  tfrqfree  29601  sstotbnd3  30272  an12i  30498  selconj  30500  2rmoswap  32189  bnj849  33983  bj-axsep  34379  islshpat  34742  islpln5  35259  islvol5  35303  cdleme0nex  36015  dicelval3  36907  mapdordlem1a  37361
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
  Copyright terms: Public domain W3C validator