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

Theorem an32s 795
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 789 . 2  |-  ( ( ( ph  /\  ch )  /\  ps )  <->  ( ( ph  /\  ps )  /\  ch ) )
2 an32s.1 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
31, 2sylbi 195 1  |-  ( ( ( ph  /\  ch )  /\  ps )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369
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 185  df-an 371
This theorem is referenced by:  anass1rs  798  anabss1  803  wereu2  4704  ordintdif  4755  ordunisssuc  4808  sossfld  5273  fssres  5566  foco  5618  dffv2  5752  fconstfv  5927  isocnv  6008  f1oiso  6029  f1ocnvfv3  6075  fun11iun  6526  onfununi  6788  oev2  6951  oaordi  6973  oaass  6988  omlimcl  7005  odi  7006  omass  7007  oewordri  7019  oelim2  7022  oeoa  7024  oeoe  7026  nnaordi  7045  omabs  7074  eceqoveq  7193  mapxpen  7465  mapdom2  7470  dif1enOLD  7532  dif1en  7533  findcard  7539  fimax2g  7546  isfinite2  7558  rankval3b  8021  isf32lem9  8518  fin1a2s  8571  zornn0g  8662  gchen1  8780  gchen2  8781  intwun  8890  suplem2pr  9210  recexsrlem  9258  axpre-sup  9324  axsup  9438  dedekind  9521  recextlem2  9955  divne0  9994  dfinfmr  10295  uzindOLD  10724  qreccl  10961  xrlttr  11105  xaddf  11182  xrsupsslem  11257  xrinfmsslem  11258  supxr2  11264  supxrunb1  11270  supxrbnd1  11272  supxrbnd2  11273  modid  11716  seqof  11847  cau3lem  12826  lo1bdd2  12986  o1co  13048  rlimcn2  13052  climcn1  13053  climcn2  13054  rlimsqzlem  13110  caucvgb  13141  fsumrlim  13257  fsumo1  13258  rplpwr  13723  dvdssq  13727  nn0seqcvgd  13728  isprm2lem  13753  isprm6  13778  phiprmpw  13834  pcneg  13923  prmpwdvds  13948  4sqlem19  14007  0ramcl  14067  imasleval  14462  catpropd  14631  funcres2c  14794  acsfiindd  15330  latdisdlem  15342  dirtr  15389  mrcmndind  15476  grpinveu  15552  mulgnn0subcl  15620  mulgsubcl  15621  mhmmulg  15639  cycsubgcl  15687  cycsubgss  15688  ghmmulg  15739  odf1  16043  dfod2  16045  gexdvds2  16064  sylow2blem3  16101  frgpup1  16252  iscyggen2  16338  iscyg3  16343  prdsgsum  16445  prdsgsumOLD  16446  rngrghm  16629  dvdsrcl2  16676  crngunit  16688  dvdsrpropd  16722  lss1d  16966  divscrng  17244  coe1tmmul  17628  mulgghm2  17767  mulgghm2OLD  17770  frgpcyg  17848  ip0r  17908  isphld  17925  frlmgsumOLD  18037  frlmgsum  18038  uvcresum  18060  tgcl  18416  0ntr  18517  innei  18571  neitr  18626  ordtrest2lem  18649  cncnp  18726  cnnei  18728  2ndcdisj  18902  dislly  18943  kgenss  18958  ptcnplem  19036  ptcnp  19037  ptcn  19042  cnmpt2k  19103  qtoprest  19132  kqt0lem  19151  isr0  19152  kqreglem1  19156  trfilss  19304  isufil2  19323  ufileu  19334  hausflim  19396  cnextcn  19481  symgtgp  19514  tsmssubm  19558  tsmsxplem1  19569  ustfilxp  19629  ustuqtop0  19657  elbl2ps  19806  elbl2  19807  nrginvrcn  20114  nmoix  20150  nmoleub  20152  cncfco  20325  icccvx  20364  iscmet3  20646  rrxmet  20749  ovolfioo  20793  ovolficc  20794  ovolicc2lem4  20845  iunmbl2  20880  dyadmax  20920  mbfsup  20984  mbflimsup  20986  mbflim  20988  itg1addlem4  21019  mbfi1flimlem  21042  itg2monolem1  21070  itg2mono  21073  itg2i1fseqle  21074  itg2i1fseq  21075  itg2addlem  21078  itg2gt0  21080  itg2cnlem1  21081  itgfsum  21146  cnlimc  21205  dvlip2  21309  itgsubst  21363  plyeq0lem  21563  plypf1  21565  dvtaylp  21720  ulmcaulem  21744  ulmcau  21745  ulmcn  21749  ulmdvlem3  21752  mtest  21754  pserulm  21772  pserdvlem2  21778  logdivlt  21955  advlogexp  21985  cxpexp  21998  cxpcl  22004  xrlimcnp  22247  basellem4  22306  logexprlim  22449  dchrsum2  22492  sumdchr2  22494  rpvmasum2  22646  pntrsumbnd2  22701  pntleml  22745  tglineeltr  22908  brbtwn2  22974  colinearalglem4  22978  axeuclidlem  23031  axcontlem8  23040  axcontlem10  23042  grpoidinvlem3  23516  grpoideu  23519  grpoinveu  23532  nmcvcn  23913  nmounbi  23999  blocnilem  24027  ubthlem1  24094  h2hlm  24205  ocsh  24509  brafnmul  25178  kbpj  25183  nmcexi  25253  lnconi  25260  riesz1  25292  mdbr2  25523  mdsl0  25537  mdslmd3i  25559  csmdsymi  25561  atcvatlem  25612  chirredlem1  25617  chirredi  25621  cdj3lem2b  25664  oduprs  25940  submarchi  26027  ordtrest2NEWlem  26206  voliune  26499  cvxscon  26980  ntrivcvg  27259  noreson  27648  btwnouttr2  27900  cgrxfr  27933  btwnxfr  27934  lineext  27954  segcon2  27983  brsegle2  27987  seglecgr12im  27988  segletr  27992  broutsideof3  28004  outsideofeu  28009  lineunray  28025  lineelsb2  28026  fin2solem  28259  heicant  28270  mblfinlem3  28274  volsupnfl  28280  itg2addnclem  28287  itg2addnclem2  28288  itg2addnclem3  28289  ftc1anclem1  28311  ftc1anclem5  28315  ftc1anclem6  28316  ftc1anc  28319  neibastop3  28427  unirep  28450  filbcmb  28478  fzmul  28480  fdc  28485  nninfnub  28491  isbnd2  28526  bndss  28529  prdsbnd  28536  prdstotbnd  28537  ismtyres  28551  rrnmet  28572  rrncmslem  28575  rrnequiv  28578  ghomco  28592  grpokerinj  28594  rngonegmn1l  28599  isdrngo2  28608  rngoisocnv  28631  divrngidl  28672  intidl  28673  unichnidl  28675  prnc  28711  isfldidl  28712  mzpindd  28927  expgrowth  29454  fnchoice  29596  stoweidlem17  29658  stoweidlem30  29671  stoweidlem38  29679  stoweidlem42  29683  stoweidlem44  29685  clwwisshclww  30317  mndpsuppss  30615  bnj110  31553  cvrexchlem  32636  ps-2  32695  3atnelvolN  32803  dib1dim  34383  dib1dim2  34386
  Copyright terms: Public domain W3C validator