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

Theorem an32s 804
Description: Swap two conjuncts in antecedent. (Contributed by NM, 13-Mar-1996.)
Hypothesis
Ref Expression
an32s.1
Assertion
Ref Expression
an32s

Proof of Theorem an32s
StepHypRef Expression
1 an32 798 . 2
2 an32s.1 . 2
31, 2sylbi 195 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369
This theorem is referenced by:  anass1rs  807  anabss1  814  wereu2  4881  ordintdif  4932  ordunisssuc  4985  sossfld  5459  fssres  5756  foco  5810  dffv2  5946  fconstfvOLD  6134  isocnv  6226  f1oiso  6247  f1ocnvfv3  6292  fun11iun  6760  onfununi  7031  oev2  7192  oaordi  7214  oaass  7229  omlimcl  7246  odi  7247  omass  7248  oewordri  7260  oelim2  7263  oeoa  7265  oeoe  7267  nnaordi  7286  omabs  7315  eceqoveq  7435  mapxpen  7703  mapdom2  7708  dif1enOLD  7772  dif1en  7773  findcard  7779  fimax2g  7786  isfinite2  7798  rankval3b  8265  isf32lem9  8762  fin1a2s  8815  zornn0g  8906  gchen1  9024  gchen2  9025  intwun  9134  suplem2pr  9452  recexsrlem  9501  axpre-sup  9567  axsup  9681  dedekind  9765  recextlem2  10205  divne0  10244  dfinfmr  10545  uzindOLD  10982  qreccl  11231  xrlttr  11375  xaddf  11452  xrsupsslem  11527  xrinfmsslem  11528  supxr2  11534  supxrunb1  11540  supxrbnd1  11542  supxrbnd2  11543  modid  12020  seqof  12164  cau3lem  13187  lo1bdd2  13347  o1co  13409  rlimcn2  13413  climcn1  13414  climcn2  13415  rlimsqzlem  13471  caucvgb  13502  fsumrlim  13625  fsumo1  13626  ntrivcvg  13706  rplpwr  14194  dvdssq  14198  nn0seqcvgd  14199  isprm2lem  14224  isprm6  14250  phiprmpw  14306  pcneg  14397  prmpwdvds  14422  4sqlem19  14481  0ramcl  14541  imasleval  14938  catpropd  15104  funcres2c  15270  acsfiindd  15807  latdisdlem  15819  dirtr  15866  mrcmndind  15997  grpinveu  16084  mulgnn0subcl  16155  mulgsubcl  16156  mhmmulg  16174  cycsubgcl  16227  cycsubgss  16228  ghmmulg  16279  odf1  16584  dfod2  16586  gexdvds2  16605  sylow2blem3  16642  frgpup1  16793  iscyggen2  16884  iscyg3  16889  prdsgsum  17007  prdsgsumOLD  17008  ringrghm  17251  dvdsrcl2  17299  crngunit  17311  dvdsrpropd  17345  lss1d  17609  quscrng  17888  coe1tmmul  18318  mulgghm2  18531  mulgghm2OLD  18534  frgpcyg  18612  ip0r  18672  isphld  18689  frlmgsumOLD  18801  frlmgsum  18802  uvcresum  18824  mdetdiagid  19102  cpmatmcllem  19219  tgcl  19471  0ntr  19572  innei  19626  neitr  19681  ordtrest2lem  19704  cncnp  19781  cnnei  19783  2ndcdisj  19957  dislly  19998  dissnlocfin  20030  kgenss  20044  ptcnplem  20122  ptcnp  20123  ptcn  20128  cnmpt2k  20189  qtoprest  20218  kqt0lem  20237  isr0  20238  kqreglem1  20242  trfilss  20390  isufil2  20409  ufileu  20420  hausflim  20482  cnextcn  20567  symgtgp  20600  tsmssubm  20644  tsmsxplem1  20655  ustfilxp  20715  ustuqtop0  20743  elbl2ps  20892  elbl2  20893  nrginvrcn  21200  nmoix  21236  nmoleub  21238  cncfco  21411  icccvx  21450  iscmet3  21732  rrxmet  21835  ovolfioo  21879  ovolficc  21880  ovolicc2lem4  21931  iunmbl2  21967  dyadmax  22007  mbfsup  22071  mbflimsup  22073  mbflim  22075  itg1addlem4  22106  mbfi1flimlem  22129  itg2monolem1  22157  itg2mono  22160  itg2i1fseqle  22161  itg2i1fseq  22162  itg2addlem  22165  itg2gt0  22167  itg2cnlem1  22168  itgfsum  22233  cnlimc  22292  dvlip2  22396  itgsubst  22450  plyeq0lem  22607  plypf1  22609  dvtaylp  22765  ulmcaulem  22789  ulmcau  22790  ulmcn  22794  ulmdvlem3  22797  mtest  22799  pserulm  22817  pserdvlem2  22823  logdivlt  23006  advlogexp  23036  cxpexp  23049  cxpcl  23055  xrlimcnp  23298  basellem4  23357  logexprlim  23500  dchrsum2  23543  sumdchr2  23545  rpvmasum2  23697  pntrsumbnd2  23752  pntleml  23796  tglineeltr  24011  brbtwn2  24208  colinearalglem4  24212  axeuclidlem  24265  axcontlem8  24274  axcontlem10  24276  clwwisshclww  24807  grpoidinvlem3  25208  grpoideu  25211  grpoinveu  25224  nmcvcn  25605  nmounbi  25691  blocnilem  25719  ubthlem1  25786  h2hlm  25897  ocsh  26201  brafnmul  26870  kbpj  26875  nmcexi  26945  lnconi  26952  riesz1  26984  mdbr2  27215  mdsl0  27229  mdslmd3i  27251  csmdsymi  27253  atcvatlem  27304  chirredlem1  27309  chirredi  27313  cdj3lem2b  27356  xrge0infss  27580  oduprs  27644  submarchi  27730  ordtrest2NEWlem  27904  voliune  28201  cvxscon  28688  noreson  29420  btwnouttr2  29672  cgrxfr  29705  btwnxfr  29706  lineext  29726  segcon2  29755  brsegle2  29759  seglecgr12im  29760  segletr  29764  broutsideof3  29776  outsideofeu  29781  lineunray  29797  lineelsb2  29798  fin2solem  30039  heicant  30049  mblfinlem3  30053  volsupnfl  30059  itg2addnclem  30066  itg2addnclem2  30067  itg2addnclem3  30068  ftc1anclem1  30090  ftc1anclem5  30094  ftc1anclem6  30095  ftc1anc  30098  neibastop3  30180  unirep  30203  filbcmb  30231  fzmul  30233  fdc  30238  nninfnub  30244  isbnd2  30279  bndss  30282  prdsbnd  30289  prdstotbnd  30290  ismtyres  30304  rrnmet  30325  rrncmslem  30328  rrnequiv  30331  ghomco  30345  grpokerinj  30347  rngonegmn1l  30352  isdrngo2  30361  rngoisocnv  30384  divrngidl  30425  intidl  30426  unichnidl  30428  prnc  30464  isfldidl  30465  mzpindd  30678  radcnvrat  31195  lcmgcdlem  31212  expgrowth  31240  fnchoice  31404  icccncfext  31690  dvnmul  31740  dvnprodlem2  31744  stoweidlem17  31799  stoweidlem30  31812  stoweidlem38  31820  stoweidlem42  31824  stoweidlem44  31826  fourierdlem31  31920  fourierdlem73  31962  fourierdlem74  31963  fourierdlem75  31964  fourierdlem83  31972  fourierdlem94  31983  fourierdlem113  32002  etransclem4  32021  initoeu2  32622  mndpsuppss  32964  aacllem  33216  bnj110  33916  cvrexchlem  35143  ps-2  35202  3atnelvolN  35310  dib1dim  36892  dib1dim2  36895
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