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  4851  sossfld  5303  ordintdif  5491  ordunisssuc  5544  fssres  5766  foco  5820  dffv2  5954  fconstfvOLD  6142  isocnv  6236  f1oiso  6257  f1ocnvfv3  6301  fun11iun  6767  onfununi  7068  oev2  7233  oaordi  7255  oaass  7270  omlimcl  7287  odi  7288  omass  7289  oewordri  7301  oelim2  7304  oeoa  7306  oeoe  7308  nnaordi  7327  omabs  7356  eceqoveq  7476  mapxpen  7744  mapdom2  7749  dif1en  7810  findcard  7816  fimax2g  7823  isfinite2  7835  rankval3b  8296  isf32lem9  8789  fin1a2s  8842  zornn0g  8933  gchen1  9049  gchen2  9050  intwun  9159  suplem2pr  9477  recexsrlem  9526  axpre-sup  9592  axsup  9708  dedekind  9796  recextlem2  10242  divne0  10281  dfinfre  10588  dfinfmrOLD  10589  qreccl  11284  xrlttr  11439  xaddf  11517  xrsupsslem  11592  xrinfmsslem  11593  supxr2  11599  supxrunb1  11605  supxrbnd1  11607  supxrbnd2  11608  modid  12118  seqof  12267  cau3lem  13396  lo1bdd2  13566  o1co  13628  rlimcn2  13632  climcn1  13633  climcn2  13634  rlimsqzlem  13690  caucvgb  13724  fsumrlim  13849  fsumo1  13850  ntrivcvg  13931  rplpwr  14495  dvdssq  14499  nn0seqcvgd  14500  lcmgcdlem  14542  isprm2lem  14602  isprm6  14637  phiprmpw  14693  pcneg  14786  prmpwdvds  14811  4sqlem19  14876  0ramcl  14944  imasleval  15398  catpropd  15565  funcres2c  15757  initoeu2  15862  acsfiindd  16374  latdisdlem  16386  dirtr  16433  mrcmndind  16564  grpinveu  16651  mulgnn0subcl  16722  mulgsubcl  16723  mhmmulg  16741  cycsubgcl  16794  cycsubgss  16795  ghmmulg  16846  odf1  17151  dfod2  17153  gexdvds2  17172  sylow2blem3  17209  frgpup1  17360  iscyggen2  17451  iscyg3  17456  prdsgsum  17545  ringrghm  17768  dvdsrcl2  17813  crngunit  17825  dvdsrpropd  17859  lss1d  18121  quscrng  18399  coe1tmmul  18805  mulgghm2  18999  frgpcyg  19075  ip0r  19135  isphld  19152  frlmgsum  19261  uvcresum  19282  mdetdiagid  19556  cpmatmcllem  19673  tgcl  19916  0ntr  20018  innei  20072  neitr  20127  ordtrest2lem  20150  cncnp  20227  cnnei  20229  2ndcdisj  20402  dislly  20443  dissnlocfin  20475  kgenss  20489  ptcnplem  20567  ptcnp  20568  ptcn  20573  cnmpt2k  20634  qtoprest  20663  kqt0lem  20682  isr0  20683  kqreglem1  20687  trfilss  20835  isufil2  20854  ufileu  20865  hausflim  20927  cnextcn  21013  symgtgp  21047  tsmssubm  21088  tsmsxplem1  21098  ustfilxp  21158  ustuqtop0  21186  elbl2ps  21335  elbl2  21336  nrginvrcn  21625  nmoix  21661  nmoleub  21663  cncfco  21835  icccvx  21874  iscmet3  22156  rrxmet  22255  ovolfioo  22299  ovolficc  22300  ovolicc2lem4  22351  iunmbl2  22387  dyadmax  22433  mbfsup  22497  mbflimsup  22500  mbflimsupOLD  22501  mbflim  22503  itg1addlem4  22534  mbfi1flimlem  22557  itg2monolem1  22585  itg2mono  22588  itg2i1fseqle  22589  itg2i1fseq  22590  itg2addlem  22593  itg2gt0  22595  itg2cnlem1  22596  itgfsum  22661  cnlimc  22720  dvlip2  22824  itgsubst  22878  plyeq0lem  23032  plypf1  23034  dvtaylp  23190  ulmcaulem  23214  ulmcau  23215  ulmcn  23219  ulmdvlem3  23222  mtest  23224  pserulm  23242  pserdvlem2  23248  logdivlt  23435  advlogexp  23465  cxpexp  23478  cxpcl  23484  xrlimcnp  23759  basellem4  23873  logexprlim  24016  dchrsum2  24059  sumdchr2  24061  rpvmasum2  24213  pntrsumbnd2  24268  pntleml  24312  tglineeltr  24535  brbtwn2  24781  colinearalglem4  24785  axeuclidlem  24838  axcontlem8  24847  axcontlem10  24849  clwwisshclww  25380  grpoidinvlem3  25779  grpoideu  25782  grpoinveu  25795  nmcvcn  26176  nmounbi  26262  blocnilem  26290  ubthlem1  26357  h2hlm  26468  ocsh  26771  brafnmul  27439  kbpj  27444  nmcexi  27514  lnconi  27521  riesz1  27553  mdbr2  27784  mdsl0  27798  mdslmd3i  27820  csmdsymi  27822  atcvatlem  27873  chirredlem1  27878  chirredi  27882  cdj3lem2b  27925  xrge0infss  28181  oduprs  28255  submarchi  28341  madjusmdetlem2  28493  ordtrest2NEWlem  28567  voliune  28891  bnj110  29457  cvxscon  29754  noreson  30334  btwnouttr2  30574  cgrxfr  30607  btwnxfr  30608  lineext  30628  segcon2  30657  brsegle2  30661  seglecgr12im  30662  segletr  30666  broutsideof3  30678  outsideofeu  30683  lineunray  30699  lineelsb2  30700  neibastop3  30803  isbasisrelowllem1  31492  isbasisrelowllem2  31493  fin2solem  31634  poimirlem4  31647  poimirlem6  31649  poimirlem7  31650  poimirlem22  31665  poimirlem23  31666  poimirlem25  31668  poimirlem26  31669  poimirlem28  31671  poimirlem30  31673  poimirlem31  31674  poimirlem32  31675  poimir  31676  broucube  31677  heicant  31678  mblfinlem3  31682  volsupnfl  31688  itg2addnclem  31696  itg2addnclem2  31697  itg2addnclem3  31698  ftc1anclem1  31720  ftc1anclem5  31724  ftc1anclem6  31725  ftc1anc  31728  unirep  31742  filbcmb  31770  fzmul  31772  fdc  31777  nninfnub  31783  isbnd2  31818  bndss  31821  prdsbnd  31828  prdstotbnd  31829  ismtyres  31843  rrnmet  31864  rrncmslem  31867  rrnequiv  31870  ghomco  31884  grpokerinj  31886  rngonegmn1l  31891  isdrngo2  31900  rngoisocnv  31923  divrngidl  31964  intidl  31965  unichnidl  31967  prnc  32003  isfldidl  32004  cvrexchlem  32692  ps-2  32751  3atnelvolN  32859  dib1dim  34441  dib1dim2  34444  mzpindd  35296  dvdsabsmod0  35545  radcnvrat  36299  expgrowth  36320  fnchoice  36989  icccncfext  37336  dvnmul  37386  dvnprodlem2  37390  stoweidlem17  37445  stoweidlem30  37459  stoweidlem38  37467  stoweidlem42  37471  stoweidlem44  37473  fourierdlem31  37568  fourierdlem73  37610  fourierdlem74  37611  fourierdlem75  37612  fourierdlem83  37620  fourierdlem94  37631  fourierdlem113  37650  etransclem4  37669  mndpsuppss  38915  aacllem  39300
  Copyright terms: Public domain W3C validator