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  4876  ordintdif  4927  ordunisssuc  4980  sossfld  5452  fssres  5749  foco  5803  dffv2  5938  fconstfv  6121  isocnv  6212  f1oiso  6233  f1ocnvfv3  6278  fun11iun  6741  onfununi  7009  oev2  7170  oaordi  7192  oaass  7207  omlimcl  7224  odi  7225  omass  7226  oewordri  7238  oelim2  7241  oeoa  7243  oeoe  7245  nnaordi  7264  omabs  7293  eceqoveq  7413  mapxpen  7680  mapdom2  7685  dif1enOLD  7748  dif1en  7749  findcard  7755  fimax2g  7762  isfinite2  7774  rankval3b  8240  isf32lem9  8737  fin1a2s  8790  zornn0g  8881  gchen1  8999  gchen2  9000  intwun  9109  suplem2pr  9427  recexsrlem  9476  axpre-sup  9542  axsup  9656  dedekind  9739  recextlem2  10176  divne0  10215  dfinfmr  10516  uzindOLD  10951  qreccl  11198  xrlttr  11342  xaddf  11419  xrsupsslem  11494  xrinfmsslem  11495  supxr2  11501  supxrunb1  11507  supxrbnd1  11509  supxrbnd2  11510  modid  11984  seqof  12128  cau3lem  13146  lo1bdd2  13306  o1co  13368  rlimcn2  13372  climcn1  13373  climcn2  13374  rlimsqzlem  13430  caucvgb  13461  fsumrlim  13584  fsumo1  13585  rplpwr  14049  dvdssq  14053  nn0seqcvgd  14054  isprm2lem  14079  isprm6  14105  phiprmpw  14161  pcneg  14252  prmpwdvds  14277  4sqlem19  14336  0ramcl  14396  imasleval  14792  catpropd  14961  funcres2c  15124  acsfiindd  15660  latdisdlem  15672  dirtr  15719  mrcmndind  15807  grpinveu  15885  mulgnn0subcl  15955  mulgsubcl  15956  mhmmulg  15974  cycsubgcl  16022  cycsubgss  16023  ghmmulg  16074  odf1  16380  dfod2  16382  gexdvds2  16401  sylow2blem3  16438  frgpup1  16589  iscyggen2  16675  iscyg3  16680  prdsgsum  16798  prdsgsumOLD  16799  rngrghm  17035  dvdsrcl2  17083  crngunit  17095  dvdsrpropd  17129  lss1d  17392  divscrng  17670  coe1tmmul  18089  mulgghm2  18298  mulgghm2OLD  18301  frgpcyg  18379  ip0r  18439  isphld  18456  frlmgsumOLD  18568  frlmgsum  18569  uvcresum  18591  mdetdiagid  18869  cpmatmcllem  18986  tgcl  19237  0ntr  19338  innei  19392  neitr  19447  ordtrest2lem  19470  cncnp  19547  cnnei  19549  2ndcdisj  19723  dislly  19764  kgenss  19779  ptcnplem  19857  ptcnp  19858  ptcn  19863  cnmpt2k  19924  qtoprest  19953  kqt0lem  19972  isr0  19973  kqreglem1  19977  trfilss  20125  isufil2  20144  ufileu  20155  hausflim  20217  cnextcn  20302  symgtgp  20335  tsmssubm  20379  tsmsxplem1  20390  ustfilxp  20450  ustuqtop0  20478  elbl2ps  20627  elbl2  20628  nrginvrcn  20935  nmoix  20971  nmoleub  20973  cncfco  21146  icccvx  21185  iscmet3  21467  rrxmet  21570  ovolfioo  21614  ovolficc  21615  ovolicc2lem4  21666  iunmbl2  21702  dyadmax  21742  mbfsup  21806  mbflimsup  21808  mbflim  21810  itg1addlem4  21841  mbfi1flimlem  21864  itg2monolem1  21892  itg2mono  21895  itg2i1fseqle  21896  itg2i1fseq  21897  itg2addlem  21900  itg2gt0  21902  itg2cnlem1  21903  itgfsum  21968  cnlimc  22027  dvlip2  22131  itgsubst  22185  plyeq0lem  22342  plypf1  22344  dvtaylp  22499  ulmcaulem  22523  ulmcau  22524  ulmcn  22528  ulmdvlem3  22531  mtest  22533  pserulm  22551  pserdvlem2  22557  logdivlt  22734  advlogexp  22764  cxpexp  22777  cxpcl  22783  xrlimcnp  23026  basellem4  23085  logexprlim  23228  dchrsum2  23271  sumdchr2  23273  rpvmasum2  23425  pntrsumbnd2  23480  pntleml  23524  tglineeltr  23725  brbtwn2  23884  colinearalglem4  23888  axeuclidlem  23941  axcontlem8  23950  axcontlem10  23952  clwwisshclww  24483  grpoidinvlem3  24884  grpoideu  24887  grpoinveu  24900  nmcvcn  25281  nmounbi  25367  blocnilem  25395  ubthlem1  25462  h2hlm  25573  ocsh  25877  brafnmul  26546  kbpj  26551  nmcexi  26621  lnconi  26628  riesz1  26660  mdbr2  26891  mdsl0  26905  mdslmd3i  26927  csmdsymi  26929  atcvatlem  26980  chirredlem1  26985  chirredi  26989  cdj3lem2b  27032  xrge0infss  27248  oduprs  27306  submarchi  27392  ordtrest2NEWlem  27540  voliune  27841  cvxscon  28328  ntrivcvg  28608  noreson  28997  btwnouttr2  29249  cgrxfr  29282  btwnxfr  29283  lineext  29303  segcon2  29332  brsegle2  29336  seglecgr12im  29337  segletr  29341  broutsideof3  29353  outsideofeu  29358  lineunray  29374  lineelsb2  29375  fin2solem  29616  heicant  29626  mblfinlem3  29630  volsupnfl  29636  itg2addnclem  29643  itg2addnclem2  29644  itg2addnclem3  29645  ftc1anclem1  29667  ftc1anclem5  29671  ftc1anclem6  29672  ftc1anc  29675  neibastop3  29783  unirep  29806  filbcmb  29834  fzmul  29836  fdc  29841  nninfnub  29847  isbnd2  29882  bndss  29885  prdsbnd  29892  prdstotbnd  29893  ismtyres  29907  rrnmet  29928  rrncmslem  29931  rrnequiv  29934  ghomco  29948  grpokerinj  29950  rngonegmn1l  29955  isdrngo2  29964  rngoisocnv  29987  divrngidl  30028  intidl  30029  unichnidl  30031  prnc  30067  isfldidl  30068  mzpindd  30282  lcmgcdlem  30812  expgrowth  30840  fnchoice  30982  icccncfext  31226  stoweidlem17  31317  stoweidlem30  31330  stoweidlem38  31338  stoweidlem42  31342  stoweidlem44  31344  fourierdlem83  31490  mndpsuppss  32037  bnj110  32995  cvrexchlem  34215  ps-2  34274  3atnelvolN  34382  dib1dim  35962  dib1dim2  35965
  Copyright terms: Public domain W3C validator