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

Theorem an32s 841
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 834 . 2 (((𝜑𝜒) ∧ 𝜓) ↔ ((𝜑𝜓) ∧ 𝜒))
2 an32s.1 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
31, 2sylbi 205 1 (((𝜑𝜒) ∧ 𝜓) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382
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 195  df-an 384
This theorem is referenced by:  anass1rs  844  anabss1  850  wereu2  5025  ordintdif  5677  ordunisssuc  5733  fssres  5968  foco  6023  dffv2  6166  isocnv  6458  f1oiso  6479  f1ocnvfv3  6523  fun11iun  6997  onfununi  7303  oev2  7468  oaordi  7491  oaass  7506  omlimcl  7523  odi  7524  omass  7525  oewordri  7537  oelim2  7540  oeoa  7542  oeoe  7544  nnaordi  7563  omabs  7592  eceqoveq  7718  mapxpen  7989  mapdom2  7994  dif1en  8056  findcard  8062  fimax2g  8069  isfinite2  8081  fimin2g  8264  rankval3b  8550  isf32lem9  9044  fin1a2s  9097  zornn0g  9188  gchen1  9304  gchen2  9305  intwun  9414  suplem2pr  9732  recexsrlem  9781  axpre-sup  9847  axsup  9965  dedekind  10052  recextlem2  10510  divne0  10549  dfinfre  10854  qreccl  11643  xrlttr  11811  xaddf  11891  xrsupsslem  11968  xrinfmsslem  11969  supxr2  11975  supxrunb1  11980  supxrbnd1  11982  supxrbnd2  11983  modid  12515  seqof  12678  cau3lem  13891  lo1bdd2  14052  o1co  14114  rlimcn2  14118  climcn1  14119  climcn2  14120  rlimsqzlem  14176  caucvgb  14207  fsumrlim  14333  fsumo1  14334  ntrivcvg  14417  rplpwr  15063  dvdssq  15067  nn0seqcvgd  15070  lcmgcdlem  15106  isprm2lem  15181  isprm6  15213  phiprmpw  15268  pcneg  15365  prmpwdvds  15395  4sqlem19  15454  0ramcl  15514  imasleval  15973  catpropd  16141  funcres2c  16333  initoeu2  16438  acsfiindd  16949  latdisdlem  16961  dirtr  17008  mrcmndind  17138  grpinveu  17228  mulgnn0subcl  17326  mulgsubcl  17327  mhmmulg  17355  cycsubgcl  17392  cycsubgss  17393  ghmmulg  17444  odf1  17751  dfod2  17753  gexdvds2  17772  sylow2blem3  17809  frgpup1  17960  iscyggen2  18055  iscyg3  18060  prdsgsum  18149  ringrghm  18377  dvdsrcl2  18422  crngunit  18434  dvdsrpropd  18468  lss1d  18733  quscrng  19010  coe1tmmul  19417  mulgghm2  19612  frgpcyg  19689  ip0r  19749  isphld  19766  frlmgsum  19878  uvcresum  19899  mdetdiagid  20173  cpmatmcllem  20290  tgcl  20532  0ntr  20633  innei  20687  neitr  20742  ordtrest2lem  20765  cncnp  20842  cnnei  20844  2ndcdisj  21017  dislly  21058  dissnlocfin  21090  kgenss  21104  ptcnplem  21182  ptcnp  21183  ptcn  21188  cnmpt2k  21249  qtoprest  21278  kqt0lem  21297  isr0  21298  kqreglem1  21302  trfilss  21451  isufil2  21470  ufileu  21481  hausflim  21543  cnextcn  21629  symgtgp  21663  tsmssubm  21704  tsmsxplem1  21714  ustfilxp  21774  ustuqtop0  21802  elbl2ps  21952  elbl2  21953  nrginvrcn  22254  nmoix  22291  nmoleub  22293  cncfco  22466  icccvx  22505  iscmet3  22844  rrxmet  22944  ovolfioo  22988  ovolficc  22989  ovolicc2lem4  23040  iunmbl2  23077  dyadmax  23117  mbfsup  23182  mbflimsup  23184  mbflim  23186  itg1addlem4  23217  mbfi1flimlem  23240  itg2monolem1  23268  itg2mono  23271  itg2i1fseqle  23272  itg2i1fseq  23273  itg2addlem  23276  itg2gt0  23278  itg2cnlem1  23279  itgfsum  23344  cnlimc  23403  dvlip2  23507  itgsubst  23561  plyeq0lem  23715  plypf1  23717  dvtaylp  23873  ulmcaulem  23897  ulmcau  23898  ulmcn  23902  ulmdvlem3  23905  mtest  23907  pserulm  23925  pserdvlem2  23931  logdivlt  24116  advlogexp  24146  cxpexp  24159  cxpcl  24165  xrlimcnp  24440  basellem4  24555  logexprlim  24695  dchrsum2  24738  sumdchr2  24740  rpvmasum2  24946  pntrsumbnd2  25001  pntleml  25045  tglineeltr  25272  brbtwn2  25531  colinearalglem4  25535  axeuclidlem  25588  axcontlem8  25597  axcontlem10  25599  clwwisshclww  26129  grpoidinvlem3  26538  grpoideu  26541  grpoinveu  26551  nmcvcn  26763  nmounbi  26849  blocnilem  26877  ubthlem1  26944  h2hlm  27055  ocsh  27360  brafnmul  28028  kbpj  28033  nmcexi  28103  lnconi  28110  riesz1  28142  mdbr2  28373  mdsl0  28387  mdslmd3i  28409  csmdsymi  28411  atcvatlem  28462  chirredlem1  28467  chirredi  28471  cdj3lem2b  28514  xrge0infss  28749  oduprs  28821  submarchi  28905  madjusmdetlem2  29056  ordtrest2NEWlem  29130  voliune  29453  bnj110  30016  cvxscon  30313  noreson  30891  btwnouttr2  31133  cgrxfr  31166  btwnxfr  31167  lineext  31187  segcon2  31216  brsegle2  31220  seglecgr12im  31221  segletr  31225  broutsideof3  31237  outsideofeu  31242  lineunray  31258  lineelsb2  31259  neibastop3  31361  isbasisrelowllem1  32203  isbasisrelowllem2  32204  unccur  32386  fin2solem  32389  matunitlindflem1  32399  matunitlindflem2  32400  poimirlem4  32407  poimirlem6  32409  poimirlem7  32410  poimirlem22  32425  poimirlem23  32426  poimirlem25  32428  poimirlem26  32429  poimirlem28  32431  poimirlem30  32433  poimirlem31  32434  poimirlem32  32435  poimir  32436  broucube  32437  heicant  32438  mblfinlem3  32442  volsupnfl  32448  itg2addnclem  32455  itg2addnclem2  32456  itg2addnclem3  32457  ftc1anclem1  32479  ftc1anclem5  32483  ftc1anclem6  32484  ftc1anc  32487  unirep  32501  filbcmb  32529  fzmul  32531  fdc  32535  nninfnub  32541  isbnd2  32576  bndss  32579  prdsbnd  32586  prdstotbnd  32587  ismtyres  32601  rrnmet  32622  rrncmslem  32625  rrnequiv  32628  ghomco  32684  grpokerinj  32686  rngonegmn1l  32734  isdrngo2  32751  rngoisocnv  32774  divrngidl  32821  intidl  32822  unichnidl  32824  prnc  32860  isfldidl  32861  cvrexchlem  33547  ps-2  33606  3atnelvolN  33714  dib1dim  35296  dib1dim2  35299  mzpindd  36151  dvdsabsmod0  36396  radcnvrat  37359  expgrowth  37380  fnchoice  38035  infxrbnd2  38350  infleinflem2  38352  xrralrecnnge  38378  icccncfext  38597  dvnmul  38657  dvnprodlem2  38661  stoweidlem17  38734  stoweidlem30  38747  stoweidlem38  38755  stoweidlem42  38759  stoweidlem44  38761  fourierdlem31  38855  fourierdlem73  38896  fourierdlem74  38897  fourierdlem75  38898  fourierdlem83  38906  fourierdlem94  38917  fourierdlem113  38936  etransclem4  38955  iinhoiicclem  39388  iccvonmbllem  39393  mndpsuppss  41968  aacllem  42339
  Copyright terms: Public domain W3C validator