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

Theorem an32s 781
Description: Swap two conjuncts in antecedent. (Contributed by NM, 13-Mar-1996.)
Hypothesis
Ref Expression
an32s.1  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
Assertion
Ref Expression
an32s  |-  ( ( ( ph  /\  ch )  /\  ps )  ->  th )

Proof of Theorem an32s
StepHypRef Expression
1 an32 775 . 2  |-  ( ( ( ph  /\  ch )  /\  ps )  <->  ( ( ph  /\  ps )  /\  ch ) )
2 an32s.1 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
31, 2sylbi 189 1  |-  ( ( ( ph  /\  ch )  /\  ps )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 6    /\ wa 360
This theorem is referenced by:  anass1rs  784  anabss1  789  wereu2  4389  ordintdif  4440  ordunisssuc  4494  sossfld  5119  fssres  5373  foco  5426  fun11iun  5458  dffv2  5553  fconstfv  5695  isocnv  5788  f1oiso  5809  f1ocnvfv3  6335  onfununi  6353  oev2  6517  oaordi  6539  oaass  6554  omlimcl  6571  odi  6572  omass  6573  oewordri  6585  oelim2  6588  oeoa  6590  oeoe  6592  nnaordi  6611  omabs  6640  eceqoveq  6758  mapxpen  7022  mapdom2  7027  dif1enOLD  7085  dif1en  7086  findcard  7092  fimax2g  7098  isfinite2  7110  rankval3b  7493  isf32lem9  7982  fin1a2s  8035  zornn0g  8127  gchen1  8242  gchen2  8243  intwun  8352  suplem2pr  8672  recexsrlem  8720  axpre-sup  8786  axsup  8893  recextlem2  9394  divne0  9431  dfinfmr  9726  uzindOLD  10101  qreccl  10331  xrlttr  10469  xaddf  10545  xrsupsslem  10619  xrinfmsslem  10620  supxr2  10626  supxrunb1  10632  supxrbnd1  10634  supxrbnd2  10635  modid  10987  seqof  11097  cau3lem  11832  lo1bdd2  11992  o1co  12054  rlimcn2  12058  climcn1  12059  climcn2  12060  rlimsqzlem  12116  caucvgb  12146  fsumrlim  12263  fsumo1  12264  rplpwr  12729  dvdssq  12733  nn0seqcvgd  12734  isprm2lem  12759  isprm6  12782  phiprmpw  12838  pcneg  12920  prmpwdvds  12945  4sqlem19  13004  0ramcl  13064  imasleval  13437  catpropd  13606  funcres2c  13769  acsfiindd  14274  latdisdlem  14286  dirtr  14352  grpinveu  14510  mulgnn0subcl  14574  mulgsubcl  14575  mhmmulg  14593  cycsubgcl  14637  cycsubgss  14638  ghmmulg  14689  odf1  14869  dfod2  14871  gexdvds2  14890  sylow2blem3  14927  frgpup1  15078  iscyggen2  15162  iscyg3  15167  prdsgsum  15223  rngrghm  15383  dvdsrcl2  15426  crngunit  15438  dvdsrpropd  15472  lss1d  15714  divscrng  15986  coe1tmmul  16347  mulgghm2  16453  frgpcyg  16521  ip0r  16535  isphld  16552  tgcl  16701  0ntr  16802  innei  16856  ordtrest2lem  16927  cncnp  17003  2ndcdisj  17176  dislly  17217  kgenss  17232  ptcnplem  17309  ptcnp  17310  ptcn  17315  cnmpt2k  17376  qtoprest  17402  kqt0lem  17421  isr0  17422  kqreglem1  17426  trfilss  17578  isufil2  17597  ufileu  17608  hausflim  17670  symgtgp  17778  tsmssubm  17819  tsmsxplem1  17829  elbl2  17944  nrginvrcn  18196  nmoix  18232  nmoleub  18234  cncfco  18405  icccvx  18442  iscmet3  18713  ovolfioo  18821  ovolficc  18822  ovolicc2lem4  18873  iunmbl2  18908  dyadmax  18947  mbfsup  19013  mbflimsup  19015  mbflim  19017  itg1addlem4  19048  mbfi1flimlem  19071  itg2monolem1  19099  itg2mono  19102  itg2i1fseqle  19103  itg2i1fseq  19104  itg2addlem  19107  itg2gt0  19109  itg2cnlem1  19110  itgfsum  19175  cnlimc  19232  dvlip2  19336  itgsubst  19390  plyeq0lem  19586  plypf1  19588  dvtaylp  19743  ulmcaulem  19765  ulmcau  19766  ulmcn  19770  ulmdvlem3  19773  mtest  19775  pserulm  19792  pserdvlem2  19798  logdivlt  19966  advlogexp  19996  cxpexp  20009  cxpcl  20015  xrlimcnp  20257  basellem4  20315  logexprlim  20458  dchrsum2  20501  sumdchr2  20503  rpvmasum2  20655  pntrsumbnd2  20710  pntleml  20754  grpoidinvlem3  20865  grpoideu  20868  grpoinveu  20881  nmcvcn  21260  nmounbi  21346  blocnilem  21374  ubthlem1  21441  h2hlm  21552  ocsh  21854  brafnmul  22523  kbpj  22528  nmcexi  22598  lnconi  22605  riesz1  22637  mdbr2  22868  mdsl0  22882  mdslmd3i  22904  csmdsymi  22906  atcvatlem  22957  chirredlem1  22962  chirredi  22966  cdj3lem2b  23009  cvxscon  23178  dedekind  23485  noreson  23714  brbtwn2  23940  colinearalglem4  23944  axeuclidlem  23997  axcontlem8  24006  axcontlem10  24008  btwnouttr2  24052  cgrxfr  24085  btwnxfr  24086  lineext  24106  segcon2  24135  brsegle2  24139  seglecgr12im  24140  segletr  24144  broutsideof3  24156  outsideofeu  24161  lineunray  24177  lineelsb2  24178  cmprtr  24795  cmperltr  24808  neibastop3  25710  unirep  25748  filbcmb  25831  fzmul  25842  fdc  25854  nninfnub  25860  isbnd2  25906  bndss  25909  prdsbnd  25916  prdstotbnd  25917  ismtyres  25931  rrnmet  25952  rrncmslem  25955  rrnequiv  25958  ghomco  25972  grpokerinj  25974  rngonegmn1l  25979  isdrngo2  25988  rngoisocnv  26011  divrngidl  26052  intidl  26053  unichnidl  26055  prnc  26091  isfldidl  26092  mzpindd  26223  frlmgsum  26631  uvcresum  26641  expgrowth  26951  stoweidlem17  27165  stoweidlem42  27190  bnj110  28157  cvrexchlem  28875  ps-2  28934  3atnelvolN  29042  dib1dim  30622  dib1dim2  30625
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10
This theorem depends on definitions:  df-bi 179  df-an 362
  Copyright terms: Public domain W3C validator