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

Theorem an32s 779
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 773 . 2  |-  ( ( ( ph  /\  ch )  /\  ps )  <->  ( ( ph  /\  ps )  /\  ch ) )
2 an32s.1 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
31, 2sylbi 187 1  |-  ( ( ( ph  /\  ch )  /\  ps )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  anass1rs  782  anabss1  787  wereu2  4406  ordintdif  4457  ordunisssuc  4511  sossfld  5136  fssres  5424  foco  5477  fun11iun  5509  dffv2  5608  fconstfv  5750  isocnv  5843  f1oiso  5864  f1ocnvfv3  6356  onfununi  6374  oev2  6538  oaordi  6560  oaass  6575  omlimcl  6592  odi  6593  omass  6594  oewordri  6606  oelim2  6609  oeoa  6611  oeoe  6613  nnaordi  6632  omabs  6661  eceqoveq  6779  mapxpen  7043  mapdom2  7048  dif1enOLD  7106  dif1en  7107  findcard  7113  fimax2g  7119  isfinite2  7131  rankval3b  7514  isf32lem9  8003  fin1a2s  8056  zornn0g  8148  gchen1  8263  gchen2  8264  intwun  8373  suplem2pr  8693  recexsrlem  8741  axpre-sup  8807  axsup  8914  recextlem2  9415  divne0  9452  dfinfmr  9747  uzindOLD  10122  qreccl  10352  xrlttr  10490  xaddf  10567  xrsupsslem  10641  xrinfmsslem  10642  supxr2  10648  supxrunb1  10654  supxrbnd1  10656  supxrbnd2  10657  modid  11009  seqof  11119  cau3lem  11854  lo1bdd2  12014  o1co  12076  rlimcn2  12080  climcn1  12081  climcn2  12082  rlimsqzlem  12138  caucvgb  12168  fsumrlim  12285  fsumo1  12286  rplpwr  12751  dvdssq  12755  nn0seqcvgd  12756  isprm2lem  12781  isprm6  12804  phiprmpw  12860  pcneg  12942  prmpwdvds  12967  4sqlem19  13026  0ramcl  13086  imasleval  13459  catpropd  13628  funcres2c  13791  acsfiindd  14296  latdisdlem  14308  dirtr  14374  grpinveu  14532  mulgnn0subcl  14596  mulgsubcl  14597  mhmmulg  14615  cycsubgcl  14659  cycsubgss  14660  ghmmulg  14711  odf1  14891  dfod2  14893  gexdvds2  14912  sylow2blem3  14949  frgpup1  15100  iscyggen2  15184  iscyg3  15189  prdsgsum  15245  rngrghm  15405  dvdsrcl2  15448  crngunit  15460  dvdsrpropd  15494  lss1d  15736  divscrng  16008  coe1tmmul  16369  mulgghm2  16475  frgpcyg  16543  ip0r  16557  isphld  16574  tgcl  16723  0ntr  16824  innei  16878  ordtrest2lem  16949  cncnp  17025  2ndcdisj  17198  dislly  17239  kgenss  17254  ptcnplem  17331  ptcnp  17332  ptcn  17337  cnmpt2k  17398  qtoprest  17424  kqt0lem  17443  isr0  17444  kqreglem1  17448  trfilss  17600  isufil2  17619  ufileu  17630  hausflim  17692  symgtgp  17800  tsmssubm  17841  tsmsxplem1  17851  elbl2  17966  nrginvrcn  18218  nmoix  18254  nmoleub  18256  cncfco  18427  icccvx  18464  iscmet3  18735  ovolfioo  18843  ovolficc  18844  ovolicc2lem4  18895  iunmbl2  18930  dyadmax  18969  mbfsup  19035  mbflimsup  19037  mbflim  19039  itg1addlem4  19070  mbfi1flimlem  19093  itg2monolem1  19121  itg2mono  19124  itg2i1fseqle  19125  itg2i1fseq  19126  itg2addlem  19129  itg2gt0  19131  itg2cnlem1  19132  itgfsum  19197  cnlimc  19254  dvlip2  19358  itgsubst  19412  plyeq0lem  19608  plypf1  19610  dvtaylp  19765  ulmcaulem  19787  ulmcau  19788  ulmcn  19792  ulmdvlem3  19795  mtest  19797  pserulm  19814  pserdvlem2  19820  logdivlt  19988  advlogexp  20018  cxpexp  20031  cxpcl  20037  xrlimcnp  20279  basellem4  20337  logexprlim  20480  dchrsum2  20523  sumdchr2  20525  rpvmasum2  20677  pntrsumbnd2  20732  pntleml  20776  grpoidinvlem3  20889  grpoideu  20892  grpoinveu  20905  nmcvcn  21284  nmounbi  21370  blocnilem  21398  ubthlem1  21465  h2hlm  21576  ocsh  21878  brafnmul  22547  kbpj  22552  nmcexi  22622  lnconi  22629  riesz1  22661  mdbr2  22892  mdsl0  22906  mdslmd3i  22928  csmdsymi  22930  atcvatlem  22981  chirredlem1  22986  chirredi  22990  cdj3lem2b  23033  cvxscon  23789  dedekind  24097  noreson  24385  brbtwn2  24605  colinearalglem4  24609  axeuclidlem  24662  axcontlem8  24671  axcontlem10  24673  btwnouttr2  24717  cgrxfr  24750  btwnxfr  24751  lineext  24771  segcon2  24800  brsegle2  24804  seglecgr12im  24805  segletr  24809  broutsideof3  24821  outsideofeu  24826  lineunray  24842  lineelsb2  24843  itg2addnclem  25003  itg2addnclem2  25004  itg2addnc  25005  cmprtr  25499  cmperltr  25512  neibastop3  26414  unirep  26452  filbcmb  26535  fzmul  26546  fdc  26558  nninfnub  26564  isbnd2  26610  bndss  26613  prdsbnd  26620  prdstotbnd  26621  ismtyres  26635  rrnmet  26656  rrncmslem  26659  rrnequiv  26662  ghomco  26676  grpokerinj  26678  rngonegmn1l  26683  isdrngo2  26692  rngoisocnv  26715  divrngidl  26756  intidl  26757  unichnidl  26759  prnc  26795  isfldidl  26796  mzpindd  26927  frlmgsum  27335  uvcresum  27345  expgrowth  27655  stoweidlem17  27869  stoweidlem42  27894  bnj110  29206  cvrexchlem  30230  ps-2  30289  3atnelvolN  30397  dib1dim  31977  dib1dim2  31980
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 177  df-an 360
  Copyright terms: Public domain W3C validator