Theorem an32s 846

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

Step	Hyp	Ref	Expression
1		an32 839	. 2 |- ( ( ( ph /\ ch ) /\ ps ) <-> ( ( ph /\ ps ) /\ ch ) )
2		an32s.1	. 2 |- ( ( ( ph /\ ps ) /\ ch ) -> th )
3	1, 2	sylbi 207	1 |- ( ( ( ph /\ ch ) /\ ps ) -> th )

Syntax hints:   -> wi 4   /\ wa 384

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 197  df-an 386

This theorem is referenced by:  anass1rs  849  anabss1  855  wereu2  5111  ordintdif  5774  ordunisssuc  5830  fssres  6070  foco  6125  dffv2  6271  isocnv  6580  f1oiso  6601  f1ocnvfv3  6646  fun11iun  7126  onfununi  7438  oev2  7603  oaordi  7626  oaass  7641  omlimcl  7658  odi  7659  omass  7660  oewordri  7672  oelim2  7675  oeoa  7677  oeoe  7679  nnaordi  7698  omabs  7727  eceqoveq  7853  mapxpen  8126  mapdom2  8131  dif1en  8193  findcard  8199  fimax2g  8206  isfinite2  8218  fimin2g  8403  rankval3b  8689  isf32lem9  9183  fin1a2s  9236  zornn0g  9327  gchen1  9447  gchen2  9448  intwun  9557  suplem2pr  9875  recexsrlem  9924  axpre-sup  9990  axsup  10113  dedekind  10200  recextlem2  10658  divne0  10697  dfinfre  11004  qreccl  11808  xrlttr  11973  xaddf  12055  xrsupsslem  12137  xrinfmsslem  12138  supxr2  12144  supxrunb1  12149  supxrbnd1  12151  supxrbnd2  12152  modid  12695  seqof  12858  cau3lem  14094  lo1bdd2  14255  o1co  14317  rlimcn2  14321  climcn1  14322  climcn2  14323  rlimsqzlem  14379  caucvgb  14410  fsumrlim  14543  fsumo1  14544  ntrivcvg  14629  rplpwr  15276  dvdssq  15280  nn0seqcvgd  15283  lcmgcdlem  15319  isprm6  15426  phiprmpw  15481  pcneg  15578  prmpwdvds  15608  4sqlem19  15667  0ramcl  15727  imasleval  16201  catpropd  16369  funcres2c  16561  initoeu2  16666  acsfiindd  17177  latdisdlem  17189  dirtr  17236  mrcmndind  17366  grpinveu  17456  mulgnn0subcl  17554  mulgsubcl  17555  mhmmulg  17583  cycsubgcl  17620  cycsubgss  17621  ghmmulg  17672  odf1  17979  dfod2  17981  gexdvds2  18000  sylow2blem3  18037  frgpup1  18188  iscyggen2  18283  iscyg3  18288  prdsgsum  18377  ringrghm  18605  dvdsrcl2  18650  crngunit  18662  dvdsrpropd  18696  lss1d  18963  quscrng  19240  coe1tmmul  19647  mulgghm2  19845  frgpcyg  19922  ip0r  19982  isphld  19999  frlmgsum  20111  uvcresum  20132  mdetdiagid  20406  cpmatmcllem  20523  tgcl  20773  0ntr  20875  innei  20929  neitr  20984  ordtrest2lem  21007  cncnp  21084  cnnei  21086  2ndcdisj  21259  dislly  21300  dissnlocfin  21332  kgenss  21346  ptcnplem  21424  ptcnp  21425  ptcn  21430  cnmpt2k  21491  qtoprest  21520  kqt0lem  21539  isr0  21540  kqreglem1  21544  trfilss  21693  isufil2  21712  ufileu  21723  hausflim  21785  cnextcn  21871  symgtgp  21905  tsmssubm  21946  tsmsxplem1  21956  ustfilxp  22016  ustuqtop0  22044  elbl2ps  22194  elbl2  22195  nrginvrcn  22496  nmoix  22533  nmoleub  22535  cncfco  22710  icccvx  22749  iscmet3  23091  rrxmet  23191  ovolfioo  23236  ovolficc  23237  ovolicc2lem4  23288  iunmbl2  23325  dyadmax  23366  mbfsup  23431  mbflimsup  23433  mbflim  23435  itg1addlem4  23466  mbfi1flimlem  23489  itg2monolem1  23517  itg2mono  23520  itg2i1fseqle  23521  itg2i1fseq  23522  itg2addlem  23525  itg2gt0  23527  itg2cnlem1  23528  itgfsum  23593  cnlimc  23652  dvlip2  23758  itgsubst  23812  plyeq0lem  23966  plypf1  23968  dvtaylp  24124  ulmcaulem  24148  ulmcau  24149  ulmcn  24153  ulmdvlem3  24156  mtest  24158  pserulm  24176  pserdvlem2  24182  logdivlt  24367  advlogexp  24401  cxpexp  24414  cxpcl  24420  xrlimcnp  24695  basellem4  24810  logexprlim  24950  dchrsum2  24993  sumdchr2  24995  rpvmasum2  25201  pntrsumbnd2  25256  pntleml  25300  tglineeltr  25526  brbtwn2  25785  colinearalglem4  25789  axeuclidlem  25842  axcontlem8  25851  axcontlem10  25853  grpoidinvlem3  27360  grpoideu  27363  grpoinveu  27373  nmcvcn  27550  nmounbi  27631  blocnilem  27659  ubthlem1  27726  h2hlm  27837  ocsh  28142  brafnmul  28810  kbpj  28815  nmcexi  28885  lnconi  28892  riesz1  28924  mdbr2  29155  mdsl0  29169  mdslmd3i  29191  csmdsymi  29193  atcvatlem  29244  chirredlem1  29249  chirredi  29253  cdj3lem2b  29296  xrge0infss  29525  oduprs  29656  submarchi  29740  madjusmdetlem2  29894  ordtrest2NEWlem  29968  voliune  30292  fsum2dsub  30685  circlemeth  30718  bnj110  30928  cvxsconn  31225  noreson  31813  btwnouttr2  32129  cgrxfr  32162  btwnxfr  32163  lineext  32183  segcon2  32212  brsegle2  32216  seglecgr12im  32217  segletr  32221  broutsideof3  32233  outsideofeu  32238  lineunray  32254  lineelsb2  32255  neibastop3  32357  isbasisrelowllem1  33203  isbasisrelowllem2  33204  unccur  33392  fin2solem  33395  matunitlindflem1  33405  matunitlindflem2  33406  poimirlem4  33413  poimirlem6  33415  poimirlem7  33416  poimirlem22  33431  poimirlem23  33432  poimirlem25  33434  poimirlem26  33435  poimirlem28  33437  poimirlem30  33439  poimirlem31  33440  poimirlem32  33441  poimir  33442  broucube  33443  heicant  33444  mblfinlem3  33448  volsupnfl  33454  itg2addnclem  33461  itg2addnclem2  33462  itg2addnclem3  33463  ftc1anclem1  33485  ftc1anclem5  33489  ftc1anclem6  33490  ftc1anc  33493  unirep  33507  filbcmb  33535  fzmul  33537  fdc  33541  nninfnub  33547  isbnd2  33582  bndss  33585  prdsbnd  33592  prdstotbnd  33593  ismtyres  33607  rrnmet  33628  rrncmslem  33631  rrnequiv  33634  ghomco  33690  grpokerinj  33692  rngonegmn1l  33740  isdrngo2  33757  rngoisocnv  33780  divrngidl  33827  intidl  33828  unichnidl  33830  prnc  33866  isfldidl  33867  cvrexchlem  34705  ps-2  34764  3atnelvolN  34872  dib1dim  36454  dib1dim2  36457  mzpindd  37309  dvdsabsmod0  37554  radcnvrat  38513  expgrowth  38534  fnchoice  39188  infxrbnd2  39585  infleinflem2  39587  xrralrecnnge  39613  limsuppnfdlem  39933  icccncfext  40100  dvnmul  40158  dvnprodlem2  40162  stoweidlem17  40234  stoweidlem30  40247  stoweidlem38  40255  stoweidlem42  40259  stoweidlem44  40261  fourierdlem31  40355  fourierdlem73  40396  fourierdlem74  40397  fourierdlem75  40398  fourierdlem83  40406  fourierdlem94  40417  fourierdlem113  40436  etransclem4  40455  iinhoiicclem  40887  iccvonmbllem  40892  smfsuplem1  41017  mndpsuppss  42152  aacllem  42547