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  4390  ordintdif  4441  ordunisssuc  4495  sossfld  5120  fssres  5408  foco  5461  fun11iun  5493  dffv2  5592  fconstfv  5734  isocnv  5827  f1oiso  5848  f1ocnvfv3  6340  onfununi  6358  oev2  6522  oaordi  6544  oaass  6559  omlimcl  6576  odi  6577  omass  6578  oewordri  6590  oelim2  6593  oeoa  6595  oeoe  6597  nnaordi  6616  omabs  6645  eceqoveq  6763  mapxpen  7027  mapdom2  7032  dif1enOLD  7090  dif1en  7091  findcard  7097  fimax2g  7103  isfinite2  7115  rankval3b  7498  isf32lem9  7987  fin1a2s  8040  zornn0g  8132  gchen1  8247  gchen2  8248  intwun  8357  suplem2pr  8677  recexsrlem  8725  axpre-sup  8791  axsup  8898  recextlem2  9399  divne0  9436  dfinfmr  9731  uzindOLD  10106  qreccl  10336  xrlttr  10474  xaddf  10551  xrsupsslem  10625  xrinfmsslem  10626  supxr2  10632  supxrunb1  10638  supxrbnd1  10640  supxrbnd2  10641  modid  10993  seqof  11103  cau3lem  11838  lo1bdd2  11998  o1co  12060  rlimcn2  12064  climcn1  12065  climcn2  12066  rlimsqzlem  12122  caucvgb  12152  fsumrlim  12269  fsumo1  12270  rplpwr  12735  dvdssq  12739  nn0seqcvgd  12740  isprm2lem  12765  isprm6  12788  phiprmpw  12844  pcneg  12926  prmpwdvds  12951  4sqlem19  13010  0ramcl  13070  imasleval  13443  catpropd  13612  funcres2c  13775  acsfiindd  14280  latdisdlem  14292  dirtr  14358  grpinveu  14516  mulgnn0subcl  14580  mulgsubcl  14581  mhmmulg  14599  cycsubgcl  14643  cycsubgss  14644  ghmmulg  14695  odf1  14875  dfod2  14877  gexdvds2  14896  sylow2blem3  14933  frgpup1  15084  iscyggen2  15168  iscyg3  15173  prdsgsum  15229  rngrghm  15389  dvdsrcl2  15432  crngunit  15444  dvdsrpropd  15478  lss1d  15720  divscrng  15992  coe1tmmul  16353  mulgghm2  16459  frgpcyg  16527  ip0r  16541  isphld  16558  tgcl  16707  0ntr  16808  innei  16862  ordtrest2lem  16933  cncnp  17009  2ndcdisj  17182  dislly  17223  kgenss  17238  ptcnplem  17315  ptcnp  17316  ptcn  17321  cnmpt2k  17382  qtoprest  17408  kqt0lem  17427  isr0  17428  kqreglem1  17432  trfilss  17584  isufil2  17603  ufileu  17614  hausflim  17676  symgtgp  17784  tsmssubm  17825  tsmsxplem1  17835  elbl2  17950  nrginvrcn  18202  nmoix  18238  nmoleub  18240  cncfco  18411  icccvx  18448  iscmet3  18719  ovolfioo  18827  ovolficc  18828  ovolicc2lem4  18879  iunmbl2  18914  dyadmax  18953  mbfsup  19019  mbflimsup  19021  mbflim  19023  itg1addlem4  19054  mbfi1flimlem  19077  itg2monolem1  19105  itg2mono  19108  itg2i1fseqle  19109  itg2i1fseq  19110  itg2addlem  19113  itg2gt0  19115  itg2cnlem1  19116  itgfsum  19181  cnlimc  19238  dvlip2  19342  itgsubst  19396  plyeq0lem  19592  plypf1  19594  dvtaylp  19749  ulmcaulem  19771  ulmcau  19772  ulmcn  19776  ulmdvlem3  19779  mtest  19781  pserulm  19798  pserdvlem2  19804  logdivlt  19972  advlogexp  20002  cxpexp  20015  cxpcl  20021  xrlimcnp  20263  basellem4  20321  logexprlim  20464  dchrsum2  20507  sumdchr2  20509  rpvmasum2  20661  pntrsumbnd2  20716  pntleml  20760  grpoidinvlem3  20873  grpoideu  20876  grpoinveu  20889  nmcvcn  21268  nmounbi  21354  blocnilem  21382  ubthlem1  21449  h2hlm  21560  ocsh  21862  brafnmul  22531  kbpj  22536  nmcexi  22606  lnconi  22613  riesz1  22645  mdbr2  22876  mdsl0  22890  mdslmd3i  22912  csmdsymi  22914  atcvatlem  22965  chirredlem1  22970  chirredi  22974  cdj3lem2b  23017  cvxscon  23774  dedekind  24082  noreson  24314  brbtwn2  24533  colinearalglem4  24537  axeuclidlem  24590  axcontlem8  24599  axcontlem10  24601  btwnouttr2  24645  cgrxfr  24678  btwnxfr  24679  lineext  24699  segcon2  24728  brsegle2  24732  seglecgr12im  24733  segletr  24737  broutsideof3  24749  outsideofeu  24754  lineunray  24770  lineelsb2  24771  cmprtr  25396  cmperltr  25409  neibastop3  26311  unirep  26349  filbcmb  26432  fzmul  26443  fdc  26455  nninfnub  26461  isbnd2  26507  bndss  26510  prdsbnd  26517  prdstotbnd  26518  ismtyres  26532  rrnmet  26553  rrncmslem  26556  rrnequiv  26559  ghomco  26573  grpokerinj  26575  rngonegmn1l  26580  isdrngo2  26589  rngoisocnv  26612  divrngidl  26653  intidl  26654  unichnidl  26656  prnc  26692  isfldidl  26693  mzpindd  26824  frlmgsum  27232  uvcresum  27242  expgrowth  27552  stoweidlem17  27766  stoweidlem42  27791  bnj110  28890  cvrexchlem  29608  ps-2  29667  3atnelvolN  29775  dib1dim  31355  dib1dim2  31358
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