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  4327  ordintdif  4378  ordunisssuc  4432  sossfld  5073  fssres  5311  foco  5364  fun11iun  5396  dffv2  5491  fconstfv  5633  isocnv  5726  f1oiso  5747  f1ocnvfv3  6273  onfununi  6291  oev2  6455  oaordi  6477  oaass  6492  omlimcl  6509  odi  6510  omass  6511  oewordri  6523  oelim2  6526  oeoa  6528  oeoe  6530  nnaordi  6549  omabs  6578  eceqoveq  6696  mapxpen  6960  mapdom2  6965  dif1enOLD  7023  dif1en  7024  findcard  7030  fimax2g  7036  isfinite2  7048  rankval3b  7431  isf32lem9  7920  fin1a2s  7973  zornn0g  8065  gchen1  8180  gchen2  8181  intwun  8290  suplem2pr  8610  recexsrlem  8658  axpre-sup  8724  axsup  8831  recextlem2  9332  divne0  9369  dfinfmr  9664  uzindOLD  10038  qreccl  10268  xrlttr  10406  xaddf  10482  xrsupsslem  10556  xrinfmsslem  10557  supxr2  10563  supxrunb1  10569  supxrbnd1  10571  supxrbnd2  10572  modid  10924  seqof  11034  cau3lem  11768  lo1bdd2  11928  o1co  11990  rlimcn2  11994  climcn1  11995  climcn2  11996  rlimsqzlem  12052  caucvgb  12082  fsumrlim  12199  fsumo1  12200  rplpwr  12662  dvdssq  12666  nn0seqcvgd  12667  isprm2lem  12692  isprm6  12715  phiprmpw  12771  pcneg  12853  prmpwdvds  12878  4sqlem19  12937  0ramcl  12997  imasleval  13370  catpropd  13539  funcres2c  13702  acsfiindd  14207  latdisdlem  14219  dirtr  14285  grpinveu  14443  mulgnn0subcl  14507  mulgsubcl  14508  mhmmulg  14526  cycsubgcl  14570  cycsubgss  14571  ghmmulg  14622  odf1  14802  dfod2  14804  gexdvds2  14823  sylow2blem3  14860  frgpup1  15011  iscyggen2  15095  iscyg3  15100  prdsgsum  15156  rngrghm  15316  dvdsrcl2  15359  crngunit  15371  dvdsrpropd  15405  lss1d  15647  divscrng  15919  coe1tmmul  16280  mulgghm2  16386  frgpcyg  16454  ip0r  16468  isphld  16485  tgcl  16634  0ntr  16735  innei  16789  ordtrest2lem  16860  cncnp  16936  2ndcdisj  17109  dislly  17150  kgenss  17165  ptcnplem  17242  ptcnp  17243  ptcn  17248  cnmpt2k  17309  qtoprest  17335  kqt0lem  17354  isr0  17355  kqreglem1  17359  trfilss  17511  isufil2  17530  ufileu  17541  hausflim  17603  symgtgp  17711  tsmssubm  17752  tsmsxplem1  17762  elbl2  17877  nrginvrcn  18129  nmoix  18165  nmoleub  18167  cncfco  18338  icccvx  18375  iscmet3  18646  ovolfioo  18754  ovolficc  18755  ovolicc2lem4  18806  iunmbl2  18841  dyadmax  18880  mbfsup  18946  mbflimsup  18948  mbflim  18950  itg1addlem4  18981  mbfi1flimlem  19004  itg2monolem1  19032  itg2mono  19035  itg2i1fseqle  19036  itg2i1fseq  19037  itg2addlem  19040  itg2gt0  19042  itg2cnlem1  19043  itgfsum  19108  cnlimc  19165  dvlip2  19269  itgsubst  19323  plyeq0lem  19519  plypf1  19521  dvtaylp  19676  ulmcaulem  19698  ulmcau  19699  ulmcn  19703  ulmdvlem3  19706  mtest  19708  pserulm  19725  pserdvlem2  19731  logdivlt  19899  advlogexp  19929  cxpexp  19942  cxpcl  19948  xrlimcnp  20190  basellem4  20248  logexprlim  20391  dchrsum2  20434  sumdchr2  20436  rpvmasum2  20588  pntrsumbnd2  20643  pntleml  20687  grpoidinvlem3  20798  grpoideu  20801  grpoinveu  20814  nmcvcn  21193  nmounbi  21279  blocnilem  21307  ubthlem1  21374  h2hlm  21485  ocsh  21787  brafnmul  22456  kbpj  22461  nmcexi  22531  lnconi  22538  riesz1  22570  mdbr2  22801  mdsl0  22815  mdslmd3i  22837  csmdsymi  22839  atcvatlem  22890  chirredlem1  22895  chirredi  22899  cdj3lem2b  22942  cvxscon  23111  dedekind  23418  noreson  23647  brbtwn2  23873  colinearalglem4  23877  axeuclidlem  23930  axcontlem8  23939  axcontlem10  23941  btwnouttr2  23985  cgrxfr  24018  btwnxfr  24019  lineext  24039  segcon2  24068  brsegle2  24072  seglecgr12im  24073  segletr  24077  broutsideof3  24089  outsideofeu  24094  lineunray  24110  lineelsb2  24111  cmprtr  24728  cmperltr  24741  neibastop3  25643  unirep  25681  filbcmb  25764  fzmul  25775  fdc  25787  nninfnub  25793  isbnd2  25839  bndss  25842  prdsbnd  25849  prdstotbnd  25850  ismtyres  25864  rrnmet  25885  rrncmslem  25888  rrnequiv  25891  ghomco  25905  grpokerinj  25907  rngonegmn1l  25912  isdrngo2  25921  rngoisocnv  25944  divrngidl  25985  intidl  25986  unichnidl  25988  prnc  26024  isfldidl  26025  mzpindd  26156  frlmgsum  26564  uvcresum  26574  expgrowth  26884  stoweidlem17  27066  stoweidlem42  27091  bnj110  27902  cvrexchlem  28738  ps-2  28797  3atnelvolN  28905  dib1dim  30485  dib1dim2  30488
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