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

Theorem an32s 818
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 812 . 2  |-  ( ( ( ph  /\  ch )  /\  ps )  <->  ( ( ph  /\  ps )  /\  ch ) )
2 an32s.1 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
31, 2sylbi 200 1  |-  ( ( ( ph  /\  ch )  /\  ps )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 375
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 190  df-an 377
This theorem is referenced by:  anass1rs  821  anabss1  828  wereu2  4853  sossfld  5305  ordintdif  5495  ordunisssuc  5548  fssres  5776  foco  5830  dffv2  5966  fconstfvOLD  6157  isocnv  6251  f1oiso  6272  f1ocnvfv3  6316  fun11iun  6785  onfununi  7091  oev2  7256  oaordi  7278  oaass  7293  omlimcl  7310  odi  7311  omass  7312  oewordri  7324  oelim2  7327  oeoa  7329  oeoe  7331  nnaordi  7350  omabs  7379  eceqoveq  7499  mapxpen  7769  mapdom2  7774  dif1en  7835  findcard  7841  fimax2g  7848  isfinite2  7860  fimin2g  8044  rankval3b  8328  isf32lem9  8822  fin1a2s  8875  zornn0g  8966  gchen1  9081  gchen2  9082  intwun  9191  suplem2pr  9509  recexsrlem  9558  axpre-sup  9624  axsup  9740  dedekind  9828  recextlem2  10276  divne0  10315  dfinfre  10621  dfinfmrOLD  10622  qreccl  11318  xrlttr  11473  xaddf  11551  xrsupsslem  11626  xrinfmsslem  11627  supxr2  11633  supxrunb1  11639  supxrbnd1  11641  supxrbnd2  11642  modid  12159  seqof  12308  cau3lem  13472  lo1bdd2  13643  o1co  13705  rlimcn2  13709  climcn1  13710  climcn2  13711  rlimsqzlem  13767  caucvgb  13801  fsumrlim  13926  fsumo1  13927  ntrivcvg  14008  rplpwr  14579  dvdssq  14583  nn0seqcvgd  14584  lcmgcdlem  14626  isprm2lem  14686  isprm6  14721  phiprmpw  14779  pcneg  14878  prmpwdvds  14903  4sqlem19  14968  0ramcl  15036  imasleval  15502  catpropd  15669  funcres2c  15861  initoeu2  15966  acsfiindd  16478  latdisdlem  16490  dirtr  16537  mrcmndind  16668  grpinveu  16755  mulgnn0subcl  16826  mulgsubcl  16827  mhmmulg  16845  cycsubgcl  16898  cycsubgss  16899  ghmmulg  16950  odf1  17268  dfod2  17270  gexdvds2  17292  sylow2blem3  17329  frgpup1  17480  iscyggen2  17571  iscyg3  17576  prdsgsum  17665  ringrghm  17888  dvdsrcl2  17933  crngunit  17945  dvdsrpropd  17979  lss1d  18241  quscrng  18519  coe1tmmul  18925  mulgghm2  19123  frgpcyg  19199  ip0r  19259  isphld  19276  frlmgsum  19385  uvcresum  19406  mdetdiagid  19680  cpmatmcllem  19797  tgcl  20040  0ntr  20142  innei  20196  neitr  20251  ordtrest2lem  20274  cncnp  20351  cnnei  20353  2ndcdisj  20526  dislly  20567  dissnlocfin  20599  kgenss  20613  ptcnplem  20691  ptcnp  20692  ptcn  20697  cnmpt2k  20758  qtoprest  20787  kqt0lem  20806  isr0  20807  kqreglem1  20811  trfilss  20959  isufil2  20978  ufileu  20989  hausflim  21051  cnextcn  21137  symgtgp  21171  tsmssubm  21212  tsmsxplem1  21222  ustfilxp  21282  ustuqtop0  21310  elbl2ps  21459  elbl2  21460  nrginvrcn  21749  nmoix  21789  nmoleub  21791  nmoixOLD  21805  nmoleubOLD  21807  cncfco  21994  icccvx  22033  iscmet3  22318  rrxmet  22417  ovolfioo  22475  ovolficc  22476  ovolicc2lem4OLD  22528  ovolicc2lem4  22529  iunmbl2  22566  dyadmax  22612  mbfsup  22676  mbflimsup  22679  mbflimsupOLD  22680  mbflim  22682  itg1addlem4  22713  mbfi1flimlem  22736  itg2monolem1  22764  itg2mono  22767  itg2i1fseqle  22768  itg2i1fseq  22769  itg2addlem  22772  itg2gt0  22774  itg2cnlem1  22775  itgfsum  22840  cnlimc  22899  dvlip2  23003  itgsubst  23057  plyeq0lem  23220  plypf1  23222  dvtaylp  23381  ulmcaulem  23405  ulmcau  23406  ulmcn  23410  ulmdvlem3  23413  mtest  23415  pserulm  23433  pserdvlem2  23439  logdivlt  23626  advlogexp  23656  cxpexp  23669  cxpcl  23675  xrlimcnp  23950  basellem4  24066  logexprlim  24209  dchrsum2  24252  sumdchr2  24254  rpvmasum2  24406  pntrsumbnd2  24461  pntleml  24505  tglineeltr  24732  brbtwn2  24991  colinearalglem4  24995  axeuclidlem  25048  axcontlem8  25057  axcontlem10  25059  clwwisshclww  25591  grpoidinvlem3  25990  grpoideu  25993  grpoinveu  26006  nmcvcn  26387  nmounbi  26473  blocnilem  26501  ubthlem1  26568  h2hlm  26689  ocsh  26992  brafnmul  27660  kbpj  27665  nmcexi  27735  lnconi  27742  riesz1  27774  mdbr2  28005  mdsl0  28019  mdslmd3i  28041  csmdsymi  28043  atcvatlem  28094  chirredlem1  28099  chirredi  28103  cdj3lem2b  28146  xrge0infss  28392  xrge0infssOLD  28393  oduprs  28469  submarchi  28554  madjusmdetlem2  28705  ordtrest2NEWlem  28779  voliune  29102  bnj110  29719  cvxscon  30016  noreson  30597  btwnouttr2  30839  cgrxfr  30872  btwnxfr  30873  lineext  30893  segcon2  30922  brsegle2  30926  seglecgr12im  30927  segletr  30931  broutsideof3  30943  outsideofeu  30948  lineunray  30964  lineelsb2  30965  neibastop3  31068  isbasisrelowllem1  31804  isbasisrelowllem2  31805  fin2solem  31977  poimirlem4  31990  poimirlem6  31992  poimirlem7  31993  poimirlem22  32008  poimirlem23  32009  poimirlem25  32011  poimirlem26  32012  poimirlem28  32014  poimirlem30  32016  poimirlem31  32017  poimirlem32  32018  poimir  32019  broucube  32020  heicant  32021  mblfinlem3  32025  volsupnfl  32031  itg2addnclem  32039  itg2addnclem2  32040  itg2addnclem3  32041  ftc1anclem1  32063  ftc1anclem5  32067  ftc1anclem6  32068  ftc1anc  32071  unirep  32085  filbcmb  32113  fzmul  32115  fdc  32120  nninfnub  32126  isbnd2  32161  bndss  32164  prdsbnd  32171  prdstotbnd  32172  ismtyres  32186  rrnmet  32207  rrncmslem  32210  rrnequiv  32213  ghomco  32227  grpokerinj  32229  rngonegmn1l  32234  isdrngo2  32243  rngoisocnv  32266  divrngidl  32307  intidl  32308  unichnidl  32310  prnc  32346  isfldidl  32347  cvrexchlem  33030  ps-2  33089  3atnelvolN  33197  dib1dim  34779  dib1dim2  34782  mzpindd  35634  dvdsabsmod0  35886  radcnvrat  36708  expgrowth  36729  fnchoice  37391  infxrbnd2  37668  infleinflem2  37670  icccncfext  37851  dvnmul  37904  dvnprodlem2  37908  stoweidlem17  37978  stoweidlem30  37992  stoweidlem38  38000  stoweidlem42  38004  stoweidlem44  38006  fourierdlem31  38101  fourierdlem31OLD  38102  fourierdlem73  38144  fourierdlem74  38145  fourierdlem75  38146  fourierdlem83  38154  fourierdlem94  38165  fourierdlem113  38184  etransclem4  38204  mndpsuppss  40525  aacllem  40909
  Copyright terms: Public domain W3C validator