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

Theorem an32s 802
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 796 . 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  805  anabss1  812  wereu2  4862  ordintdif  4913  ordunisssuc  4966  sossfld  5440  fssres  5737  foco  5791  dffv2  5927  fconstfvOLD  6114  isocnv  6207  f1oiso  6228  f1ocnvfv3  6273  fun11iun  6741  onfununi  7010  oev2  7171  oaordi  7193  oaass  7208  omlimcl  7225  odi  7226  omass  7227  oewordri  7239  oelim2  7242  oeoa  7244  oeoe  7246  nnaordi  7265  omabs  7294  eceqoveq  7414  mapxpen  7681  mapdom2  7686  dif1enOLD  7750  dif1en  7751  findcard  7757  fimax2g  7764  isfinite2  7776  rankval3b  8242  isf32lem9  8739  fin1a2s  8792  zornn0g  8883  gchen1  9001  gchen2  9002  intwun  9111  suplem2pr  9429  recexsrlem  9478  axpre-sup  9544  axsup  9658  dedekind  9742  recextlem2  10181  divne0  10220  dfinfmr  10521  uzindOLD  10958  qreccl  11206  xrlttr  11350  xaddf  11427  xrsupsslem  11502  xrinfmsslem  11503  supxr2  11509  supxrunb1  11515  supxrbnd1  11517  supxrbnd2  11518  modid  11994  seqof  12138  cau3lem  13161  lo1bdd2  13321  o1co  13383  rlimcn2  13387  climcn1  13388  climcn2  13389  rlimsqzlem  13445  caucvgb  13476  fsumrlim  13599  fsumo1  13600  rplpwr  14066  dvdssq  14070  nn0seqcvgd  14071  isprm2lem  14096  isprm6  14122  phiprmpw  14178  pcneg  14269  prmpwdvds  14294  4sqlem19  14353  0ramcl  14413  imasleval  14810  catpropd  14976  funcres2c  15139  acsfiindd  15676  latdisdlem  15688  dirtr  15735  mrcmndind  15866  grpinveu  15953  mulgnn0subcl  16024  mulgsubcl  16025  mhmmulg  16043  cycsubgcl  16096  cycsubgss  16097  ghmmulg  16148  odf1  16453  dfod2  16455  gexdvds2  16474  sylow2blem3  16511  frgpup1  16662  iscyggen2  16753  iscyg3  16758  prdsgsum  16876  prdsgsumOLD  16877  ringrghm  17119  dvdsrcl2  17167  crngunit  17179  dvdsrpropd  17213  lss1d  17477  quscrng  17756  coe1tmmul  18186  mulgghm2  18398  mulgghm2OLD  18401  frgpcyg  18479  ip0r  18539  isphld  18556  frlmgsumOLD  18668  frlmgsum  18669  uvcresum  18691  mdetdiagid  18969  cpmatmcllem  19086  tgcl  19337  0ntr  19438  innei  19492  neitr  19547  ordtrest2lem  19570  cncnp  19647  cnnei  19649  2ndcdisj  19823  dislly  19864  dissnlocfin  19896  kgenss  19910  ptcnplem  19988  ptcnp  19989  ptcn  19994  cnmpt2k  20055  qtoprest  20084  kqt0lem  20103  isr0  20104  kqreglem1  20108  trfilss  20256  isufil2  20275  ufileu  20286  hausflim  20348  cnextcn  20433  symgtgp  20466  tsmssubm  20510  tsmsxplem1  20521  ustfilxp  20581  ustuqtop0  20609  elbl2ps  20758  elbl2  20759  nrginvrcn  21066  nmoix  21102  nmoleub  21104  cncfco  21277  icccvx  21316  iscmet3  21598  rrxmet  21701  ovolfioo  21745  ovolficc  21746  ovolicc2lem4  21797  iunmbl2  21833  dyadmax  21873  mbfsup  21937  mbflimsup  21939  mbflim  21941  itg1addlem4  21972  mbfi1flimlem  21995  itg2monolem1  22023  itg2mono  22026  itg2i1fseqle  22027  itg2i1fseq  22028  itg2addlem  22031  itg2gt0  22033  itg2cnlem1  22034  itgfsum  22099  cnlimc  22158  dvlip2  22262  itgsubst  22316  plyeq0lem  22473  plypf1  22475  dvtaylp  22630  ulmcaulem  22654  ulmcau  22655  ulmcn  22659  ulmdvlem3  22662  mtest  22664  pserulm  22682  pserdvlem2  22688  logdivlt  22871  advlogexp  22901  cxpexp  22914  cxpcl  22920  xrlimcnp  23163  basellem4  23222  logexprlim  23365  dchrsum2  23408  sumdchr2  23410  rpvmasum2  23562  pntrsumbnd2  23617  pntleml  23661  tglineeltr  23876  brbtwn2  24073  colinearalglem4  24077  axeuclidlem  24130  axcontlem8  24139  axcontlem10  24141  clwwisshclww  24672  grpoidinvlem3  25073  grpoideu  25076  grpoinveu  25089  nmcvcn  25470  nmounbi  25556  blocnilem  25584  ubthlem1  25651  h2hlm  25762  ocsh  26066  brafnmul  26735  kbpj  26740  nmcexi  26810  lnconi  26817  riesz1  26849  mdbr2  27080  mdsl0  27094  mdslmd3i  27116  csmdsymi  27118  atcvatlem  27169  chirredlem1  27174  chirredi  27178  cdj3lem2b  27221  xrge0infss  27445  oduprs  27510  submarchi  27596  ordtrest2NEWlem  27770  voliune  28067  cvxscon  28554  ntrivcvg  28999  noreson  29388  btwnouttr2  29640  cgrxfr  29673  btwnxfr  29674  lineext  29694  segcon2  29723  brsegle2  29727  seglecgr12im  29728  segletr  29732  broutsideof3  29744  outsideofeu  29749  lineunray  29765  lineelsb2  29766  fin2solem  30007  heicant  30017  mblfinlem3  30021  volsupnfl  30027  itg2addnclem  30034  itg2addnclem2  30035  itg2addnclem3  30036  ftc1anclem1  30058  ftc1anclem5  30062  ftc1anclem6  30063  ftc1anc  30066  neibastop3  30148  unirep  30171  filbcmb  30199  fzmul  30201  fdc  30206  nninfnub  30212  isbnd2  30247  bndss  30250  prdsbnd  30257  prdstotbnd  30258  ismtyres  30272  rrnmet  30293  rrncmslem  30296  rrnequiv  30299  ghomco  30313  grpokerinj  30315  rngonegmn1l  30320  isdrngo2  30329  rngoisocnv  30352  divrngidl  30393  intidl  30394  unichnidl  30396  prnc  30432  isfldidl  30433  mzpindd  30646  radcnvrat  31164  lcmgcdlem  31181  expgrowth  31209  fnchoice  31351  icccncfext  31593  stoweidlem17  31684  stoweidlem30  31697  stoweidlem38  31705  stoweidlem42  31709  stoweidlem44  31711  fourierdlem31  31805  fourierdlem73  31847  fourierdlem74  31848  fourierdlem75  31849  fourierdlem83  31857  fourierdlem94  31868  fourierdlem113  31887  mndpsuppss  32674  bnj110  33623  cvrexchlem  34845  ps-2  34904  3atnelvolN  35012  dib1dim  36594  dib1dim2  36597
  Copyright terms: Public domain W3C validator