MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  an32s Structured version   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 4    /\ wa 360
This theorem is referenced by:  anass1rs  784  anabss1  789  wereu2  4580  ordintdif  4631  ordunisssuc  4685  sossfld  5318  fssres  5611  foco  5664  fun11iun  5696  dffv2  5797  fconstfv  5955  isocnv  6051  f1oiso  6072  f1ocnvfv3  6586  onfununi  6604  oev2  6768  oaordi  6790  oaass  6805  omlimcl  6822  odi  6823  omass  6824  oewordri  6836  oelim2  6839  oeoa  6841  oeoe  6843  nnaordi  6862  omabs  6891  eceqoveq  7010  mapxpen  7274  mapdom2  7279  dif1enOLD  7341  dif1en  7342  findcard  7348  fimax2g  7354  isfinite2  7366  rankval3b  7753  isf32lem9  8242  fin1a2s  8295  zornn0g  8386  gchen1  8501  gchen2  8502  intwun  8611  suplem2pr  8931  recexsrlem  8979  axpre-sup  9045  axsup  9152  recextlem2  9654  divne0  9691  dfinfmr  9986  uzindOLD  10365  qreccl  10595  xrlttr  10734  xaddf  10811  xrsupsslem  10886  xrinfmsslem  10887  supxr2  10893  supxrunb1  10899  supxrbnd1  10901  supxrbnd2  10902  modid  11271  seqof  11381  cau3lem  12159  lo1bdd2  12319  o1co  12381  rlimcn2  12385  climcn1  12386  climcn2  12387  rlimsqzlem  12443  caucvgb  12474  fsumrlim  12591  fsumo1  12592  rplpwr  13057  dvdssq  13061  nn0seqcvgd  13062  isprm2lem  13087  isprm6  13110  phiprmpw  13166  pcneg  13248  prmpwdvds  13273  4sqlem19  13332  0ramcl  13392  imasleval  13767  catpropd  13936  funcres2c  14099  acsfiindd  14604  latdisdlem  14616  dirtr  14682  grpinveu  14840  mulgnn0subcl  14904  mulgsubcl  14905  mhmmulg  14923  cycsubgcl  14967  cycsubgss  14968  ghmmulg  15019  odf1  15199  dfod2  15201  gexdvds2  15220  sylow2blem3  15257  frgpup1  15408  iscyggen2  15492  iscyg3  15497  prdsgsum  15553  rngrghm  15713  dvdsrcl2  15756  crngunit  15768  dvdsrpropd  15802  lss1d  16040  divscrng  16312  coe1tmmul  16670  mulgghm2  16787  frgpcyg  16855  ip0r  16869  isphld  16886  tgcl  17035  0ntr  17136  innei  17190  neitr  17245  ordtrest2lem  17268  cncnp  17345  cnnei  17347  2ndcdisj  17520  dislly  17561  kgenss  17576  ptcnplem  17654  ptcnp  17655  ptcn  17660  cnmpt2k  17721  qtoprest  17750  kqt0lem  17769  isr0  17770  kqreglem1  17774  trfilss  17922  isufil2  17941  ufileu  17952  hausflim  18014  cnextcn  18099  symgtgp  18132  tsmssubm  18173  tsmsxplem1  18183  ustfilxp  18243  ustuqtop0  18271  elbl2ps  18420  elbl2  18421  nrginvrcn  18728  nmoix  18764  nmoleub  18766  cncfco  18938  icccvx  18976  iscmet3  19247  ovolfioo  19365  ovolficc  19366  ovolicc2lem4  19417  iunmbl2  19452  dyadmax  19491  mbfsup  19557  mbflimsup  19559  mbflim  19561  itg1addlem4  19592  mbfi1flimlem  19615  itg2monolem1  19643  itg2mono  19646  itg2i1fseqle  19647  itg2i1fseq  19648  itg2addlem  19651  itg2gt0  19653  itg2cnlem1  19654  itgfsum  19719  cnlimc  19776  dvlip2  19880  itgsubst  19934  plyeq0lem  20130  plypf1  20132  dvtaylp  20287  ulmcaulem  20311  ulmcau  20312  ulmcn  20316  ulmdvlem3  20319  mtest  20321  pserulm  20339  pserdvlem2  20345  logdivlt  20517  advlogexp  20547  cxpexp  20560  cxpcl  20566  xrlimcnp  20808  basellem4  20867  logexprlim  21010  dchrsum2  21053  sumdchr2  21055  rpvmasum2  21207  pntrsumbnd2  21262  pntleml  21306  grpoidinvlem3  21795  grpoideu  21798  grpoinveu  21811  nmcvcn  22192  nmounbi  22278  blocnilem  22306  ubthlem1  22373  h2hlm  22484  ocsh  22786  brafnmul  23455  kbpj  23460  nmcexi  23530  lnconi  23537  riesz1  23569  mdbr2  23800  mdsl0  23814  mdslmd3i  23836  csmdsymi  23838  atcvatlem  23889  chirredlem1  23894  chirredi  23898  cdj3lem2b  23941  voliune  24586  cvxscon  24931  dedekind  25188  ntrivcvg  25226  noreson  25616  brbtwn2  25845  colinearalglem4  25849  axeuclidlem  25902  axcontlem8  25911  axcontlem10  25913  btwnouttr2  25957  cgrxfr  25990  btwnxfr  25991  lineext  26011  segcon2  26040  brsegle2  26044  seglecgr12im  26045  segletr  26049  broutsideof3  26061  outsideofeu  26066  lineunray  26082  lineelsb2  26083  mblfinlem3  26246  volsupnfl  26252  itg2addnclem  26257  itg2addnclem2  26258  itg2addnclem3  26259  ftc1anclem1  26281  ftc1anclem2  26282  ftc1anclem5  26285  ftc1anclem6  26286  ftc1anc  26289  neibastop3  26392  unirep  26415  filbcmb  26443  fzmul  26445  fdc  26450  nninfnub  26456  isbnd2  26493  bndss  26496  prdsbnd  26503  prdstotbnd  26504  ismtyres  26518  rrnmet  26539  rrncmslem  26542  rrnequiv  26545  ghomco  26559  grpokerinj  26561  rngonegmn1l  26566  isdrngo2  26575  rngoisocnv  26598  divrngidl  26639  intidl  26640  unichnidl  26642  prnc  26678  isfldidl  26679  mzpindd  26804  frlmgsum  27210  uvcresum  27220  expgrowth  27530  fnchoice  27677  stoweidlem17  27743  stoweidlem30  27756  stoweidlem38  27764  stoweidlem42  27768  stoweidlem44  27770  bnj110  29230  cvrexchlem  30217  ps-2  30276  3atnelvolN  30384  dib1dim  31964  dib1dim2  31967
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 179  df-an 362
  Copyright terms: Public domain W3C validator