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

Theorem an32s 811
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 805 . 2  |-  ( ( ( ph  /\  ch )  /\  ps )  <->  ( ( ph  /\  ps )  /\  ch ) )
2 an32s.1 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
31, 2sylbi 198 1  |-  ( ( ( ph  /\  ch )  /\  ps )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370
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 188  df-an 372
This theorem is referenced by:  anass1rs  814  anabss1  821  wereu2  4850  sossfld  5302  ordintdif  5491  ordunisssuc  5544  fssres  5766  foco  5820  dffv2  5954  fconstfvOLD  6142  isocnv  6236  f1oiso  6257  f1ocnvfv3  6301  fun11iun  6767  onfununi  7071  oev2  7236  oaordi  7258  oaass  7273  omlimcl  7290  odi  7291  omass  7292  oewordri  7304  oelim2  7307  oeoa  7309  oeoe  7311  nnaordi  7330  omabs  7359  eceqoveq  7479  mapxpen  7747  mapdom2  7752  dif1en  7813  findcard  7819  fimax2g  7826  isfinite2  7838  fimin2g  8022  rankval3b  8305  isf32lem9  8798  fin1a2s  8851  zornn0g  8942  gchen1  9057  gchen2  9058  intwun  9167  suplem2pr  9485  recexsrlem  9534  axpre-sup  9600  axsup  9716  dedekind  9804  recextlem2  10250  divne0  10289  dfinfre  10595  dfinfmrOLD  10596  qreccl  11291  xrlttr  11446  xaddf  11524  xrsupsslem  11599  xrinfmsslem  11600  supxr2  11606  supxrunb1  11612  supxrbnd1  11614  supxrbnd2  11615  modid  12127  seqof  12276  cau3lem  13417  lo1bdd2  13587  o1co  13649  rlimcn2  13653  climcn1  13654  climcn2  13655  rlimsqzlem  13711  caucvgb  13745  fsumrlim  13870  fsumo1  13871  ntrivcvg  13952  rplpwr  14523  dvdssq  14527  nn0seqcvgd  14528  lcmgcdlem  14570  isprm2lem  14630  isprm6  14665  phiprmpw  14723  pcneg  14822  prmpwdvds  14847  4sqlem19  14912  0ramcl  14980  imasleval  15446  catpropd  15613  funcres2c  15805  initoeu2  15910  acsfiindd  16422  latdisdlem  16434  dirtr  16481  mrcmndind  16612  grpinveu  16699  mulgnn0subcl  16770  mulgsubcl  16771  mhmmulg  16789  cycsubgcl  16842  cycsubgss  16843  ghmmulg  16894  odf1  17212  dfod2  17214  gexdvds2  17236  sylow2blem3  17273  frgpup1  17424  iscyggen2  17515  iscyg3  17520  prdsgsum  17609  ringrghm  17832  dvdsrcl2  17877  crngunit  17889  dvdsrpropd  17923  lss1d  18185  quscrng  18463  coe1tmmul  18869  mulgghm2  19066  frgpcyg  19142  ip0r  19202  isphld  19219  frlmgsum  19328  uvcresum  19349  mdetdiagid  19623  cpmatmcllem  19740  tgcl  19983  0ntr  20085  innei  20139  neitr  20194  ordtrest2lem  20217  cncnp  20294  cnnei  20296  2ndcdisj  20469  dislly  20510  dissnlocfin  20542  kgenss  20556  ptcnplem  20634  ptcnp  20635  ptcn  20640  cnmpt2k  20701  qtoprest  20730  kqt0lem  20749  isr0  20750  kqreglem1  20754  trfilss  20902  isufil2  20921  ufileu  20932  hausflim  20994  cnextcn  21080  symgtgp  21114  tsmssubm  21155  tsmsxplem1  21165  ustfilxp  21225  ustuqtop0  21253  elbl2ps  21402  elbl2  21403  nrginvrcn  21692  nmoix  21732  nmoleub  21734  nmoixOLD  21748  nmoleubOLD  21750  cncfco  21937  icccvx  21976  iscmet3  22261  rrxmet  22360  ovolfioo  22418  ovolficc  22419  ovolicc2lem4OLD  22471  ovolicc2lem4  22472  iunmbl2  22508  dyadmax  22554  mbfsup  22618  mbflimsup  22621  mbflimsupOLD  22622  mbflim  22624  itg1addlem4  22655  mbfi1flimlem  22678  itg2monolem1  22706  itg2mono  22709  itg2i1fseqle  22710  itg2i1fseq  22711  itg2addlem  22714  itg2gt0  22716  itg2cnlem1  22717  itgfsum  22782  cnlimc  22841  dvlip2  22945  itgsubst  22999  plyeq0lem  23162  plypf1  23164  dvtaylp  23323  ulmcaulem  23347  ulmcau  23348  ulmcn  23352  ulmdvlem3  23355  mtest  23357  pserulm  23375  pserdvlem2  23381  logdivlt  23568  advlogexp  23598  cxpexp  23611  cxpcl  23617  xrlimcnp  23892  basellem4  24008  logexprlim  24151  dchrsum2  24194  sumdchr2  24196  rpvmasum2  24348  pntrsumbnd2  24403  pntleml  24447  tglineeltr  24674  brbtwn2  24933  colinearalglem4  24937  axeuclidlem  24990  axcontlem8  24999  axcontlem10  25001  clwwisshclww  25533  grpoidinvlem3  25932  grpoideu  25935  grpoinveu  25948  nmcvcn  26329  nmounbi  26415  blocnilem  26443  ubthlem1  26510  h2hlm  26631  ocsh  26934  brafnmul  27602  kbpj  27607  nmcexi  27677  lnconi  27684  riesz1  27716  mdbr2  27947  mdsl0  27961  mdslmd3i  27983  csmdsymi  27985  atcvatlem  28036  chirredlem1  28041  chirredi  28045  cdj3lem2b  28088  xrge0infss  28346  xrge0infssOLD  28347  oduprs  28424  submarchi  28510  madjusmdetlem2  28662  ordtrest2NEWlem  28736  voliune  29060  bnj110  29677  cvxscon  29974  noreson  30554  btwnouttr2  30794  cgrxfr  30827  btwnxfr  30828  lineext  30848  segcon2  30877  brsegle2  30881  seglecgr12im  30882  segletr  30886  broutsideof3  30898  outsideofeu  30903  lineunray  30919  lineelsb2  30920  neibastop3  31023  isbasisrelowllem1  31722  isbasisrelowllem2  31723  fin2solem  31895  poimirlem4  31908  poimirlem6  31910  poimirlem7  31911  poimirlem22  31926  poimirlem23  31927  poimirlem25  31929  poimirlem26  31930  poimirlem28  31932  poimirlem30  31934  poimirlem31  31935  poimirlem32  31936  poimir  31937  broucube  31938  heicant  31939  mblfinlem3  31943  volsupnfl  31949  itg2addnclem  31957  itg2addnclem2  31958  itg2addnclem3  31959  ftc1anclem1  31981  ftc1anclem5  31985  ftc1anclem6  31986  ftc1anc  31989  unirep  32003  filbcmb  32031  fzmul  32033  fdc  32038  nninfnub  32044  isbnd2  32079  bndss  32082  prdsbnd  32089  prdstotbnd  32090  ismtyres  32104  rrnmet  32125  rrncmslem  32128  rrnequiv  32131  ghomco  32145  grpokerinj  32147  rngonegmn1l  32152  isdrngo2  32161  rngoisocnv  32184  divrngidl  32225  intidl  32226  unichnidl  32228  prnc  32264  isfldidl  32265  cvrexchlem  32953  ps-2  33012  3atnelvolN  33120  dib1dim  34702  dib1dim2  34705  mzpindd  35557  dvdsabsmod0  35810  radcnvrat  36633  expgrowth  36654  fnchoice  37323  icccncfext  37705  dvnmul  37758  dvnprodlem2  37762  stoweidlem17  37817  stoweidlem30  37831  stoweidlem38  37839  stoweidlem42  37843  stoweidlem44  37845  fourierdlem31  37940  fourierdlem31OLD  37941  fourierdlem73  37983  fourierdlem74  37984  fourierdlem75  37985  fourierdlem83  37993  fourierdlem94  38004  fourierdlem113  38023  etransclem4  38043  mndpsuppss  39778  aacllem  40162
  Copyright terms: Public domain W3C validator