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  4348  ordintdif  4399  ordunisssuc  4453  sossfld  5094  fssres  5332  foco  5385  fun11iun  5417  dffv2  5512  fconstfv  5654  isocnv  5747  f1oiso  5768  f1ocnvfv3  6294  onfununi  6312  oev2  6476  oaordi  6498  oaass  6513  omlimcl  6530  odi  6531  omass  6532  oewordri  6544  oelim2  6547  oeoa  6549  oeoe  6551  nnaordi  6570  omabs  6599  eceqoveq  6717  mapxpen  6981  mapdom2  6986  dif1enOLD  7044  dif1en  7045  findcard  7051  fimax2g  7057  isfinite2  7069  rankval3b  7452  isf32lem9  7941  fin1a2s  7994  zornn0g  8086  gchen1  8201  gchen2  8202  intwun  8311  suplem2pr  8631  recexsrlem  8679  axpre-sup  8745  axsup  8852  recextlem2  9353  divne0  9390  dfinfmr  9685  uzindOLD  10059  qreccl  10289  xrlttr  10427  xaddf  10503  xrsupsslem  10577  xrinfmsslem  10578  supxr2  10584  supxrunb1  10590  supxrbnd1  10592  supxrbnd2  10593  modid  10945  seqof  11055  cau3lem  11789  lo1bdd2  11949  o1co  12011  rlimcn2  12015  climcn1  12016  climcn2  12017  rlimsqzlem  12073  caucvgb  12103  fsumrlim  12220  fsumo1  12221  rplpwr  12683  dvdssq  12687  nn0seqcvgd  12688  isprm2lem  12713  isprm6  12736  phiprmpw  12792  pcneg  12874  prmpwdvds  12899  4sqlem19  12958  0ramcl  13018  imasleval  13391  catpropd  13560  funcres2c  13723  acsfiindd  14228  latdisdlem  14240  dirtr  14306  grpinveu  14464  mulgnn0subcl  14528  mulgsubcl  14529  mhmmulg  14547  cycsubgcl  14591  cycsubgss  14592  ghmmulg  14643  odf1  14823  dfod2  14825  gexdvds2  14844  sylow2blem3  14881  frgpup1  15032  iscyggen2  15116  iscyg3  15121  prdsgsum  15177  rngrghm  15337  dvdsrcl2  15380  crngunit  15392  dvdsrpropd  15426  lss1d  15668  divscrng  15940  coe1tmmul  16301  mulgghm2  16407  frgpcyg  16475  ip0r  16489  isphld  16506  tgcl  16655  0ntr  16756  innei  16810  ordtrest2lem  16881  cncnp  16957  2ndcdisj  17130  dislly  17171  kgenss  17186  ptcnplem  17263  ptcnp  17264  ptcn  17269  cnmpt2k  17330  qtoprest  17356  kqt0lem  17375  isr0  17376  kqreglem1  17380  trfilss  17532  isufil2  17551  ufileu  17562  hausflim  17624  symgtgp  17732  tsmssubm  17773  tsmsxplem1  17783  elbl2  17898  nrginvrcn  18150  nmoix  18186  nmoleub  18188  cncfco  18359  icccvx  18396  iscmet3  18667  ovolfioo  18775  ovolficc  18776  ovolicc2lem4  18827  iunmbl2  18862  dyadmax  18901  mbfsup  18967  mbflimsup  18969  mbflim  18971  itg1addlem4  19002  mbfi1flimlem  19025  itg2monolem1  19053  itg2mono  19056  itg2i1fseqle  19057  itg2i1fseq  19058  itg2addlem  19061  itg2gt0  19063  itg2cnlem1  19064  itgfsum  19129  cnlimc  19186  dvlip2  19290  itgsubst  19344  plyeq0lem  19540  plypf1  19542  dvtaylp  19697  ulmcaulem  19719  ulmcau  19720  ulmcn  19724  ulmdvlem3  19727  mtest  19729  pserulm  19746  pserdvlem2  19752  logdivlt  19920  advlogexp  19950  cxpexp  19963  cxpcl  19969  xrlimcnp  20211  basellem4  20269  logexprlim  20412  dchrsum2  20455  sumdchr2  20457  rpvmasum2  20609  pntrsumbnd2  20664  pntleml  20708  grpoidinvlem3  20819  grpoideu  20822  grpoinveu  20835  nmcvcn  21214  nmounbi  21300  blocnilem  21328  ubthlem1  21395  h2hlm  21506  ocsh  21808  brafnmul  22477  kbpj  22482  nmcexi  22552  lnconi  22559  riesz1  22591  mdbr2  22822  mdsl0  22836  mdslmd3i  22858  csmdsymi  22860  atcvatlem  22911  chirredlem1  22916  chirredi  22920  cdj3lem2b  22963  cvxscon  23132  dedekind  23439  noreson  23668  brbtwn2  23894  colinearalglem4  23898  axeuclidlem  23951  axcontlem8  23960  axcontlem10  23962  btwnouttr2  24006  cgrxfr  24039  btwnxfr  24040  lineext  24060  segcon2  24089  brsegle2  24093  seglecgr12im  24094  segletr  24098  broutsideof3  24110  outsideofeu  24115  lineunray  24131  lineelsb2  24132  cmprtr  24749  cmperltr  24762  neibastop3  25664  unirep  25702  filbcmb  25785  fzmul  25796  fdc  25808  nninfnub  25814  isbnd2  25860  bndss  25863  prdsbnd  25870  prdstotbnd  25871  ismtyres  25885  rrnmet  25906  rrncmslem  25909  rrnequiv  25912  ghomco  25926  grpokerinj  25928  rngonegmn1l  25933  isdrngo2  25942  rngoisocnv  25965  divrngidl  26006  intidl  26007  unichnidl  26009  prnc  26045  isfldidl  26046  mzpindd  26177  frlmgsum  26585  uvcresum  26595  expgrowth  26905  stoweidlem17  27087  stoweidlem42  27112  bnj110  27923  cvrexchlem  28759  ps-2  28818  3atnelvolN  28926  dib1dim  30506  dib1dim2  30509
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