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  810  wereu2  4712  ordintdif  4763  ordunisssuc  4816  sossfld  5280  fssres  5573  foco  5625  dffv2  5759  fconstfv  5935  isocnv  6016  f1oiso  6037  f1ocnvfv3  6082  fun11iun  6532  onfununi  6794  oev2  6955  oaordi  6977  oaass  6992  omlimcl  7009  odi  7010  omass  7011  oewordri  7023  oelim2  7026  oeoa  7028  oeoe  7030  nnaordi  7049  omabs  7078  eceqoveq  7197  mapxpen  7469  mapdom2  7474  dif1enOLD  7536  dif1en  7537  findcard  7543  fimax2g  7550  isfinite2  7562  rankval3b  8025  isf32lem9  8522  fin1a2s  8575  zornn0g  8666  gchen1  8784  gchen2  8785  intwun  8894  suplem2pr  9214  recexsrlem  9262  axpre-sup  9328  axsup  9442  dedekind  9525  recextlem2  9959  divne0  9998  dfinfmr  10299  uzindOLD  10728  qreccl  10965  xrlttr  11109  xaddf  11186  xrsupsslem  11261  xrinfmsslem  11262  supxr2  11268  supxrunb1  11274  supxrbnd1  11276  supxrbnd2  11277  modid  11724  seqof  11855  cau3lem  12834  lo1bdd2  12994  o1co  13056  rlimcn2  13060  climcn1  13061  climcn2  13062  rlimsqzlem  13118  caucvgb  13149  fsumrlim  13266  fsumo1  13267  rplpwr  13732  dvdssq  13736  nn0seqcvgd  13737  isprm2lem  13762  isprm6  13787  phiprmpw  13843  pcneg  13932  prmpwdvds  13957  4sqlem19  14016  0ramcl  14076  imasleval  14471  catpropd  14640  funcres2c  14803  acsfiindd  15339  latdisdlem  15351  dirtr  15398  mrcmndind  15485  grpinveu  15563  mulgnn0subcl  15631  mulgsubcl  15632  mhmmulg  15650  cycsubgcl  15698  cycsubgss  15699  ghmmulg  15750  odf1  16054  dfod2  16056  gexdvds2  16075  sylow2blem3  16112  frgpup1  16263  iscyggen2  16349  iscyg3  16354  prdsgsum  16459  prdsgsumOLD  16460  rngrghm  16682  dvdsrcl2  16730  crngunit  16742  dvdsrpropd  16776  lss1d  17021  divscrng  17299  coe1tmmul  17705  mulgghm2  17900  mulgghm2OLD  17903  frgpcyg  17981  ip0r  18041  isphld  18058  frlmgsumOLD  18170  frlmgsum  18171  uvcresum  18193  tgcl  18549  0ntr  18650  innei  18704  neitr  18759  ordtrest2lem  18782  cncnp  18859  cnnei  18861  2ndcdisj  19035  dislly  19076  kgenss  19091  ptcnplem  19169  ptcnp  19170  ptcn  19175  cnmpt2k  19236  qtoprest  19265  kqt0lem  19284  isr0  19285  kqreglem1  19289  trfilss  19437  isufil2  19456  ufileu  19467  hausflim  19529  cnextcn  19614  symgtgp  19647  tsmssubm  19691  tsmsxplem1  19702  ustfilxp  19762  ustuqtop0  19790  elbl2ps  19939  elbl2  19940  nrginvrcn  20247  nmoix  20283  nmoleub  20285  cncfco  20458  icccvx  20497  iscmet3  20779  rrxmet  20882  ovolfioo  20926  ovolficc  20927  ovolicc2lem4  20978  iunmbl2  21013  dyadmax  21053  mbfsup  21117  mbflimsup  21119  mbflim  21121  itg1addlem4  21152  mbfi1flimlem  21175  itg2monolem1  21203  itg2mono  21206  itg2i1fseqle  21207  itg2i1fseq  21208  itg2addlem  21211  itg2gt0  21213  itg2cnlem1  21214  itgfsum  21279  cnlimc  21338  dvlip2  21442  itgsubst  21496  plyeq0lem  21653  plypf1  21655  dvtaylp  21810  ulmcaulem  21834  ulmcau  21835  ulmcn  21839  ulmdvlem3  21842  mtest  21844  pserulm  21862  pserdvlem2  21868  logdivlt  22045  advlogexp  22075  cxpexp  22088  cxpcl  22094  xrlimcnp  22337  basellem4  22396  logexprlim  22539  dchrsum2  22582  sumdchr2  22584  rpvmasum2  22736  pntrsumbnd2  22791  pntleml  22835  tglineeltr  23007  brbtwn2  23102  colinearalglem4  23106  axeuclidlem  23159  axcontlem8  23168  axcontlem10  23170  grpoidinvlem3  23644  grpoideu  23647  grpoinveu  23660  nmcvcn  24041  nmounbi  24127  blocnilem  24155  ubthlem1  24222  h2hlm  24333  ocsh  24637  brafnmul  25306  kbpj  25311  nmcexi  25381  lnconi  25388  riesz1  25420  mdbr2  25651  mdsl0  25665  mdslmd3i  25687  csmdsymi  25689  atcvatlem  25740  chirredlem1  25745  chirredi  25749  cdj3lem2b  25792  xrge0infss  26004  oduprs  26068  submarchi  26154  ordtrest2NEWlem  26304  voliune  26597  cvxscon  27084  ntrivcvg  27363  noreson  27752  btwnouttr2  28004  cgrxfr  28037  btwnxfr  28038  lineext  28058  segcon2  28087  brsegle2  28091  seglecgr12im  28092  segletr  28096  broutsideof3  28108  outsideofeu  28113  lineunray  28129  lineelsb2  28130  fin2solem  28368  heicant  28379  mblfinlem3  28383  volsupnfl  28389  itg2addnclem  28396  itg2addnclem2  28397  itg2addnclem3  28398  ftc1anclem1  28420  ftc1anclem5  28424  ftc1anclem6  28425  ftc1anc  28428  neibastop3  28536  unirep  28559  filbcmb  28587  fzmul  28589  fdc  28594  nninfnub  28600  isbnd2  28635  bndss  28638  prdsbnd  28645  prdstotbnd  28646  ismtyres  28660  rrnmet  28681  rrncmslem  28684  rrnequiv  28687  ghomco  28701  grpokerinj  28703  rngonegmn1l  28708  isdrngo2  28717  rngoisocnv  28740  divrngidl  28781  intidl  28782  unichnidl  28784  prnc  28820  isfldidl  28821  mzpindd  29035  expgrowth  29562  fnchoice  29704  stoweidlem17  29765  stoweidlem30  29778  stoweidlem38  29786  stoweidlem42  29790  stoweidlem44  29792  clwwisshclww  30424  mndpsuppss  30735  mdetdiagid  30826  bnj110  31738  cvrexchlem  32903  ps-2  32962  3atnelvolN  33070  dib1dim  34650  dib1dim2  34653
  Copyright terms: Public domain W3C validator