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

Theorem an32s 782
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 776 . 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  785  anabss1  790  wereu2  4283  ordintdif  4334  ordunisssuc  4386  sossfld  5027  fssres  5265  foco  5318  fun11iun  5350  dffv2  5444  fconstfv  5586  isocnv  5679  f1oiso  5700  f1ocnvfv3  6226  onfununi  6244  oev2  6408  oaordi  6430  oaass  6445  omlimcl  6462  odi  6463  omass  6464  oewordri  6476  oelim2  6479  oeoa  6481  oeoe  6483  nnaordi  6502  omabs  6531  eceqoveq  6649  mapxpen  6912  mapdom2  6917  dif1enOLD  6975  dif1en  6976  findcard  6982  fimax2g  6988  isfinite2  7000  rankval3b  7382  isf32lem9  7871  fin1a2s  7924  zornn0g  8016  gchen1  8127  gchen2  8128  intwun  8237  suplem2pr  8557  recexsrlem  8605  axpre-sup  8671  axsup  8778  recextlem2  9279  divne0  9316  dfinfmr  9611  uzindOLD  9985  qreccl  10215  xrlttr  10353  xaddf  10429  xrsupsslem  10503  xrinfmsslem  10504  supxr2  10510  supxrunb1  10516  supxrbnd1  10518  supxrbnd2  10519  modid  10871  seqof  10981  cau3lem  11715  lo1bdd2  11875  o1co  11937  rlimcn2  11941  climcn1  11942  climcn2  11943  rlimsqzlem  11999  caucvgb  12029  fsumrlim  12146  fsumo1  12147  rplpwr  12609  dvdssq  12613  nn0seqcvgd  12614  isprm2lem  12639  isprm6  12662  phiprmpw  12718  pcneg  12800  prmpwdvds  12825  4sqlem19  12884  0ramcl  12944  imasleval  13317  catpropd  13456  funcres2c  13619  latdisdlem  14127  dirtr  14193  grpinveu  14351  mulgnn0subcl  14415  mulgsubcl  14416  mhmmulg  14434  cycsubgcl  14478  cycsubgss  14479  ghmmulg  14530  odf1  14710  dfod2  14712  gexdvds2  14731  sylow2blem3  14768  frgpup1  14919  iscyggen2  15003  iscyg3  15008  prdsgsum  15064  rngrghm  15224  dvdsrcl2  15267  crngunit  15279  dvdsrpropd  15313  lss1d  15555  divscrng  15824  coe1tmmul  16185  mulgghm2  16291  frgpcyg  16359  ip0r  16373  isphld  16390  tgcl  16539  0ntr  16640  innei  16694  ordtrest2lem  16765  cncnp  16841  2ndcdisj  17014  dislly  17055  kgenss  17070  ptcnplem  17147  ptcnp  17148  ptcn  17153  cnmpt2k  17214  qtoprest  17240  kqt0lem  17259  isr0  17260  kqreglem1  17264  trfilss  17416  isufil2  17435  ufileu  17446  hausflim  17508  symgtgp  17616  tsmssubm  17657  tsmsxplem1  17667  elbl2  17782  nrginvrcn  18034  nmoix  18070  nmoleub  18072  cncfco  18243  icccvx  18280  iscmet3  18551  ovolfioo  18659  ovolficc  18660  ovolicc2lem4  18711  iunmbl2  18746  dyadmax  18785  mbfsup  18851  mbflimsup  18853  mbflim  18855  itg1addlem4  18886  mbfi1flimlem  18909  itg2monolem1  18937  itg2mono  18940  itg2i1fseqle  18941  itg2i1fseq  18942  itg2addlem  18945  itg2gt0  18947  itg2cnlem1  18948  itgfsum  19013  cnlimc  19070  dvlip2  19174  itgsubst  19228  plyeq0lem  19424  plypf1  19426  dvtaylp  19581  ulmcaulem  19603  ulmcau  19604  ulmcn  19608  ulmdvlem3  19611  mtest  19613  pserulm  19630  pserdvlem2  19636  logdivlt  19804  advlogexp  19834  cxpexp  19883  cxpcl  19889  xrlimcnp  20095  basellem4  20153  logexprlim  20296  dchrsum2  20339  sumdchr2  20341  rpvmasum2  20493  pntrsumbnd2  20548  pntleml  20592  grpoidinvlem3  20703  grpoideu  20706  grpoinveu  20719  nmcvcn  21098  nmounbi  21184  blocnilem  21212  ubthlem1  21279  h2hlm  21390  ocsh  21692  brafnmul  22361  kbpj  22366  nmcexi  22436  lnconi  22443  riesz1  22475  mdbr2  22706  mdsl0  22720  mdslmd3i  22742  csmdsymi  22744  atcvatlem  22795  chirredlem1  22800  chirredi  22804  cdj3lem2b  22847  cvxscon  22945  dedekind  23252  noreson  23481  brbtwn2  23707  colinearalglem4  23711  axeuclidlem  23764  axcontlem8  23773  axcontlem10  23775  btwnouttr2  23819  cgrxfr  23852  btwnxfr  23853  lineext  23873  segcon2  23902  brsegle2  23906  seglecgr12im  23907  segletr  23911  broutsideof3  23923  outsideofeu  23928  lineunray  23944  lineelsb2  23945  cmprtr  24562  cmperltr  24575  neibastop3  25477  unirep  25515  filbcmb  25598  fzmul  25609  fdc  25621  nninfnub  25627  isbnd2  25673  bndss  25676  prdsbnd  25683  prdstotbnd  25684  ismtyres  25698  rrnmet  25719  rrncmslem  25722  rrnequiv  25725  ghomco  25739  grpokerinj  25741  rngonegmn1l  25746  isdrngo2  25755  rngoisocnv  25778  divrngidl  25819  intidl  25820  unichnidl  25822  prnc  25858  isfldidl  25859  mzpindd  25990  frlmgsum  26398  uvcresum  26408  expgrowth  26718  bnj110  27579  cvrexchlem  28297  ps-2  28356  3atnelvolN  28464  dib1dim  30044  dib1dim2  30047
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