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

Theorem an32s 650
Description: Swap two conjuncts in antecedent. (Contributed by NM, 13-Mar-1996.)
Hypothesis
Ref Expression
an32s.1 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
Assertion
Ref Expression
an32s (((𝜑𝜒) ∧ 𝜓) → 𝜃)

Proof of Theorem an32s
StepHypRef Expression
1 an32 644 . 2 (((𝜑𝜒) ∧ 𝜓) ↔ ((𝜑𝜓) ∧ 𝜒))
2 an32s.1 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
31, 2sylbi 216 1 (((𝜑𝜒) ∧ 𝜓) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397
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 206  df-an 398
This theorem is referenced by:  anass1rs  653  anabss1  664  biadanid  821  wereu2  5593  ordintdif  6326  ordunisssuc  6381  fssres  6666  dffv2  6891  isocnv  7229  f1oiso  7250  f1ocnvfv3  7299  fiunlem  7812  onfununi  8199  oev2  8380  oaordi  8404  oaass  8419  omlimcl  8436  odi  8437  omass  8438  oewordri  8450  oelim2  8453  oeoa  8455  oeoe  8457  nnaordi  8476  omabs  8508  eceqoveq  8638  mapxpen  8964  mapdom2  8969  findcard  8980  dif1enALT  9090  fimax2g  9100  isfinite2  9112  fimin2g  9296  rankval3b  9624  isf32lem9  10159  fin1a2s  10212  zornn0g  10303  gchen1  10423  gchen2  10424  intwun  10533  suplem2pr  10851  recexsrlem  10901  axpre-sup  10967  axsup  11092  dedekind  11180  recextlem2  11648  divne0  11687  dfinfre  11998  qreccl  12751  xrlttr  12916  xaddf  13000  xrsupsslem  13083  xrinfmsslem  13084  supxr2  13090  supxrunb1  13095  supxrbnd1  13097  supxrbnd2  13098  modid  13658  seqof  13822  cau3lem  15107  lo1bdd2  15274  o1co  15336  rlimcn3  15340  climcn1  15342  climcn2  15343  rlimsqzlem  15401  caucvgb  15432  fsumrlim  15564  fsumo1  15565  ntrivcvg  15650  rplpwr  16308  dvdssq  16313  nn0seqcvgd  16316  lcmgcdlem  16352  isprm6  16460  phiprmpw  16518  pcneg  16616  prmpwdvds  16646  4sqlem19  16705  0ramcl  16765  imasleval  17293  catpropd  17459  funcres2c  17658  initoeu2  17772  latdisdlem  18255  acsfiindd  18312  dirtr  18361  mndind  18507  grpinveu  18655  mulgnn0subcl  18758  mulgsubcl  18759  mhmmulg  18785  cycsubm  18862  cycsubgcl  18866  cycsubgss  18867  ghmmulg  18887  odf1  19210  dfod2  19212  gexdvds2  19231  sylow2blem3  19268  frgpup1  19422  iscyggen2  19522  iscyg3  19527  prdsgsum  19623  ringrghm  19885  dvdsrcl2  19933  crngunit  19945  dvdsrpropd  19979  lss1d  20266  quscrng  20552  mulgghm2  20739  frgpcyg  20822  ip0r  20883  isphld  20900  frlmgsum  21020  uvcresum  21041  coe1tmmul  21489  mdetdiagid  21790  cpmatmcllem  21908  tgcl  22160  0ntr  22263  innei  22317  neitr  22372  ordtrest2lem  22395  cncnp  22472  cnnei  22474  2ndcdisj  22648  dislly  22689  dissnlocfin  22721  kgenss  22735  ptcnplem  22813  ptcnp  22814  ptcn  22819  cnmpt2k  22880  qtoprest  22909  kqt0lem  22928  isr0  22929  kqreglem1  22933  trfilss  23081  isufil2  23100  ufileu  23111  hausflim  23173  cnextcn  23259  symgtgp  23298  tsmssubm  23335  tsmsxplem1  23345  ustfilxp  23405  ustuqtop0  23433  elbl2ps  23583  elbl2  23584  nrginvrcn  23897  nmoix  23934  nmoleub  23936  cncfco  24111  icccvx  24154  iscmet3  24498  rrxmet  24613  ovolfioo  24672  ovolficc  24673  ovolicc2lem4  24725  iunmbl2  24762  dyadmax  24803  mbfsup  24869  mbflimsup  24871  mbflim  24873  itg1addlem4  24904  itg1addlem4OLD  24905  mbfi1flimlem  24928  itg2monolem1  24956  itg2mono  24959  itg2i1fseqle  24960  itg2i1fseq  24961  itg2addlem  24964  itg2gt0  24966  itg2cnlem1  24967  itgfsum  25032  cnlimc  25093  dvlip2  25200  itgsubst  25254  plyeq0lem  25412  plypf1  25414  dvtaylp  25570  ulmcaulem  25594  ulmcau  25595  ulmcn  25599  ulmdvlem3  25602  mtest  25604  pserulm  25622  pserdvlem2  25628  logdivlt  25817  advlogexp  25851  cxpexp  25864  cxpcl  25870  xrlimcnp  26159  basellem4  26274  logexprlim  26414  dchrsum2  26457  sumdchr2  26459  rpvmasum2  26701  pntrsumbnd2  26756  pntleml  26800  tglineeltr  27033  brbtwn2  27314  colinearalglem4  27318  axeuclidlem  27371  axcontlem8  27380  axcontlem10  27382  grpoidinvlem3  28909  grpoideu  28912  grpoinveu  28922  nmcvcn  29098  nmounbi  29179  blocnilem  29207  ubthlem1  29273  h2hlm  29383  ocsh  29686  brafnmul  30354  kbpj  30359  nmcexi  30429  lnconi  30436  riesz1  30468  mdbr2  30699  mdsl0  30713  mdslmd3i  30735  csmdsymi  30737  atcvatlem  30788  chirredlem1  30793  chirredi  30797  cdj3lem2b  30840  xrge0infss  31124  oduprs  31283  mgcmntco  31313  lmodvslmhm  31351  submarchi  31481  grplsm0l  31632  ssmxidllem  31682  lindsunlem  31746  lindsun  31747  madjusmdetlem2  31819  zarcmplem  31872  ordtrest2NEWlem  31913  voliune  32238  fsum2dsub  32628  circlemeth  32661  bnj110  32879  cvxsconn  33246  noreson  33904  btwnouttr2  34365  cgrxfr  34398  btwnxfr  34399  lineext  34419  segcon2  34448  brsegle2  34452  seglecgr12im  34453  segletr  34457  broutsideof3  34469  outsideofeu  34474  lineunray  34490  lineelsb2  34491  neibastop3  34592  bj-imdiridlem  35397  isbasisrelowllem1  35567  isbasisrelowllem2  35568  fvineqsneu  35623  unccur  35801  fin2solem  35804  lindsadd  35811  matunitlindflem1  35814  matunitlindflem2  35815  poimirlem4  35822  poimirlem6  35824  poimirlem7  35825  poimirlem22  35840  poimirlem23  35841  poimirlem25  35843  poimirlem26  35844  poimirlem28  35846  poimirlem30  35848  poimirlem31  35849  poimirlem32  35850  poimir  35851  broucube  35852  heicant  35853  mblfinlem3  35857  volsupnfl  35863  itg2addnclem  35869  itg2addnclem2  35870  itg2addnclem3  35871  ftc1anclem1  35891  ftc1anclem5  35895  ftc1anclem6  35896  ftc1anc  35899  unirep  35912  filbcmb  35939  fzmul  35940  fdc  35944  nninfnub  35950  isbnd2  35982  bndss  35985  prdsbnd  35992  prdstotbnd  35993  ismtyres  36007  rrnmet  36028  rrncmslem  36031  rrnequiv  36034  ghomco  36090  grpokerinj  36092  rngonegmn1l  36140  isdrngo2  36157  rngoisocnv  36180  divrngidl  36227  intidl  36228  unichnidl  36230  prnc  36266  isfldidl  36267  cvrexchlem  37472  ps-2  37531  3atnelvolN  37639  dib1dim  39218  dib1dim2  39221  pwsgprod  40305  fsuppind  40315  mzpindd  40604  dvdsabsmod0  40846  radcnvrat  41969  expgrowth  41990  fnchoice  42609  infxrbnd2  42955  infleinflem2  42957  xrralrecnnge  42977  limsuppnfdlem  43290  icccncfext  43476  dvnmul  43532  dvnprodlem2  43536  stoweidlem17  43606  stoweidlem30  43619  stoweidlem38  43627  stoweidlem42  43631  stoweidlem44  43633  fourierdlem31  43727  fourierdlem73  43768  fourierdlem74  43769  fourierdlem75  43770  fourierdlem83  43778  fourierdlem94  43789  fourierdlem113  43808  etransclem4  43827  iinhoiicclem  44260  iccvonmbllem  44265  smfsuplem1  44397  mndpsuppss  45764  itsclquadeu  46180  aacllem  46562
  Copyright terms: Public domain W3C validator