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

Theorem an32s 780
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 774 . 2  |-  ( ( ( ph  /\  ch )  /\  ps )  <->  ( ( ph  /\  ps )  /\  ch ) )
2 an32s.1 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
31, 2sylbi 188 1  |-  ( ( ( ph  /\  ch )  /\  ps )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  anass1rs  783  anabss1  788  wereu2  4539  ordintdif  4590  ordunisssuc  4643  sossfld  5276  fssres  5569  foco  5622  fun11iun  5654  dffv2  5755  fconstfv  5913  isocnv  6009  f1oiso  6030  f1ocnvfv3  6544  onfununi  6562  oev2  6726  oaordi  6748  oaass  6763  omlimcl  6780  odi  6781  omass  6782  oewordri  6794  oelim2  6797  oeoa  6799  oeoe  6801  nnaordi  6820  omabs  6849  eceqoveq  6968  mapxpen  7232  mapdom2  7237  dif1enOLD  7299  dif1en  7300  findcard  7306  fimax2g  7312  isfinite2  7324  rankval3b  7708  isf32lem9  8197  fin1a2s  8250  zornn0g  8341  gchen1  8456  gchen2  8457  intwun  8566  suplem2pr  8886  recexsrlem  8934  axpre-sup  9000  axsup  9107  recextlem2  9609  divne0  9646  dfinfmr  9941  uzindOLD  10320  qreccl  10550  xrlttr  10689  xaddf  10766  xrsupsslem  10841  xrinfmsslem  10842  supxr2  10848  supxrunb1  10854  supxrbnd1  10856  supxrbnd2  10857  modid  11225  seqof  11335  cau3lem  12113  lo1bdd2  12273  o1co  12335  rlimcn2  12339  climcn1  12340  climcn2  12341  rlimsqzlem  12397  caucvgb  12428  fsumrlim  12545  fsumo1  12546  rplpwr  13011  dvdssq  13015  nn0seqcvgd  13016  isprm2lem  13041  isprm6  13064  phiprmpw  13120  pcneg  13202  prmpwdvds  13227  4sqlem19  13286  0ramcl  13346  imasleval  13721  catpropd  13890  funcres2c  14053  acsfiindd  14558  latdisdlem  14570  dirtr  14636  grpinveu  14794  mulgnn0subcl  14858  mulgsubcl  14859  mhmmulg  14877  cycsubgcl  14921  cycsubgss  14922  ghmmulg  14973  odf1  15153  dfod2  15155  gexdvds2  15174  sylow2blem3  15211  frgpup1  15362  iscyggen2  15446  iscyg3  15451  prdsgsum  15507  rngrghm  15667  dvdsrcl2  15710  crngunit  15722  dvdsrpropd  15756  lss1d  15994  divscrng  16266  coe1tmmul  16624  mulgghm2  16741  frgpcyg  16809  ip0r  16823  isphld  16840  tgcl  16989  0ntr  17090  innei  17144  neitr  17198  ordtrest2lem  17221  cncnp  17298  cnnei  17300  2ndcdisj  17472  dislly  17513  kgenss  17528  ptcnplem  17606  ptcnp  17607  ptcn  17612  cnmpt2k  17673  qtoprest  17702  kqt0lem  17721  isr0  17722  kqreglem1  17726  trfilss  17874  isufil2  17893  ufileu  17904  hausflim  17966  cnextcn  18051  symgtgp  18084  tsmssubm  18125  tsmsxplem1  18135  ustfilxp  18195  ustuqtop0  18223  elbl2ps  18372  elbl2  18373  nrginvrcn  18680  nmoix  18716  nmoleub  18718  cncfco  18890  icccvx  18928  iscmet3  19199  ovolfioo  19317  ovolficc  19318  ovolicc2lem4  19369  iunmbl2  19404  dyadmax  19443  mbfsup  19509  mbflimsup  19511  mbflim  19513  itg1addlem4  19544  mbfi1flimlem  19567  itg2monolem1  19595  itg2mono  19598  itg2i1fseqle  19599  itg2i1fseq  19600  itg2addlem  19603  itg2gt0  19605  itg2cnlem1  19606  itgfsum  19671  cnlimc  19728  dvlip2  19832  itgsubst  19886  plyeq0lem  20082  plypf1  20084  dvtaylp  20239  ulmcaulem  20263  ulmcau  20264  ulmcn  20268  ulmdvlem3  20271  mtest  20273  pserulm  20291  pserdvlem2  20297  logdivlt  20469  advlogexp  20499  cxpexp  20512  cxpcl  20518  xrlimcnp  20760  basellem4  20819  logexprlim  20962  dchrsum2  21005  sumdchr2  21007  rpvmasum2  21159  pntrsumbnd2  21214  pntleml  21258  grpoidinvlem3  21747  grpoideu  21750  grpoinveu  21763  nmcvcn  22144  nmounbi  22230  blocnilem  22258  ubthlem1  22325  h2hlm  22436  ocsh  22738  brafnmul  23407  kbpj  23412  nmcexi  23482  lnconi  23489  riesz1  23521  mdbr2  23752  mdsl0  23766  mdslmd3i  23788  csmdsymi  23790  atcvatlem  23841  chirredlem1  23846  chirredi  23850  cdj3lem2b  23893  voliune  24538  cvxscon  24883  dedekind  25140  ntrivcvg  25178  noreson  25528  brbtwn2  25748  colinearalglem4  25752  axeuclidlem  25805  axcontlem8  25814  axcontlem10  25816  btwnouttr2  25860  cgrxfr  25893  btwnxfr  25894  lineext  25914  segcon2  25943  brsegle2  25947  seglecgr12im  25948  segletr  25952  broutsideof3  25964  outsideofeu  25969  lineunray  25985  lineelsb2  25986  mblfinlem2  26144  volsupnfl  26150  itg2addnclem  26155  itg2addnclem2  26156  itg2addnclem3  26157  neibastop3  26281  unirep  26304  filbcmb  26332  fzmul  26334  fdc  26339  nninfnub  26345  isbnd2  26382  bndss  26385  prdsbnd  26392  prdstotbnd  26393  ismtyres  26407  rrnmet  26428  rrncmslem  26431  rrnequiv  26434  ghomco  26448  grpokerinj  26450  rngonegmn1l  26455  isdrngo2  26464  rngoisocnv  26487  divrngidl  26528  intidl  26529  unichnidl  26531  prnc  26567  isfldidl  26568  mzpindd  26693  frlmgsum  27100  uvcresum  27110  expgrowth  27420  fnchoice  27567  stoweidlem17  27633  stoweidlem30  27646  stoweidlem38  27654  stoweidlem42  27658  stoweidlem44  27660  bnj110  28935  cvrexchlem  29901  ps-2  29960  3atnelvolN  30068  dib1dim  31648  dib1dim2  31651
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 178  df-an 361
  Copyright terms: Public domain W3C validator