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

Theorem an32s 863
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 856 . 2 (((𝜑𝜒) ∧ 𝜓) ↔ ((𝜑𝜓) ∧ 𝜒))
2 an32s.1 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
31, 2sylbi 207 1 (((𝜑𝜒) ∧ 𝜓) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383
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 197  df-an 385
This theorem is referenced by:  anass1rs  866  anabss1  872  wereu2  5140  ordintdif  5812  ordunisssuc  5868  fssres  6108  foco  6163  dffv2  6310  isocnv  6620  f1oiso  6641  f1ocnvfv3  6686  fun11iun  7168  onfununi  7483  oev2  7648  oaordi  7671  oaass  7686  omlimcl  7703  odi  7704  omass  7705  oewordri  7717  oelim2  7720  oeoa  7722  oeoe  7724  nnaordi  7743  omabs  7772  eceqoveq  7895  mapxpen  8167  mapdom2  8172  dif1en  8234  findcard  8240  fimax2g  8247  isfinite2  8259  fimin2g  8444  rankval3b  8727  isf32lem9  9221  fin1a2s  9274  zornn0g  9365  gchen1  9485  gchen2  9486  intwun  9595  suplem2pr  9913  recexsrlem  9962  axpre-sup  10028  axsup  10151  dedekind  10238  recextlem2  10696  divne0  10735  dfinfre  11042  qreccl  11846  xrlttr  12011  xaddf  12093  xrsupsslem  12175  xrinfmsslem  12176  supxr2  12182  supxrunb1  12187  supxrbnd1  12189  supxrbnd2  12190  modid  12735  seqof  12898  cau3lem  14138  lo1bdd2  14299  o1co  14361  rlimcn2  14365  climcn1  14366  climcn2  14367  rlimsqzlem  14423  caucvgb  14454  fsumrlim  14587  fsumo1  14588  ntrivcvg  14673  rplpwr  15323  dvdssq  15327  nn0seqcvgd  15330  lcmgcdlem  15366  isprm6  15473  phiprmpw  15528  pcneg  15625  prmpwdvds  15655  4sqlem19  15714  0ramcl  15774  imasleval  16248  catpropd  16416  funcres2c  16608  initoeu2  16713  acsfiindd  17224  latdisdlem  17236  dirtr  17283  mrcmndind  17413  grpinveu  17503  mulgnn0subcl  17601  mulgsubcl  17602  mhmmulg  17630  cycsubgcl  17667  cycsubgss  17668  ghmmulg  17719  odf1  18025  dfod2  18027  gexdvds2  18046  sylow2blem3  18083  frgpup1  18234  iscyggen2  18329  iscyg3  18334  prdsgsum  18423  ringrghm  18651  dvdsrcl2  18696  crngunit  18708  dvdsrpropd  18742  lss1d  19011  quscrng  19288  coe1tmmul  19695  mulgghm2  19893  frgpcyg  19970  ip0r  20030  isphld  20047  frlmgsum  20159  uvcresum  20180  mdetdiagid  20454  cpmatmcllem  20571  tgcl  20821  0ntr  20923  innei  20977  neitr  21032  ordtrest2lem  21055  cncnp  21132  cnnei  21134  2ndcdisj  21307  dislly  21348  dissnlocfin  21380  kgenss  21394  ptcnplem  21472  ptcnp  21473  ptcn  21478  cnmpt2k  21539  qtoprest  21568  kqt0lem  21587  isr0  21588  kqreglem1  21592  trfilss  21740  isufil2  21759  ufileu  21770  hausflim  21832  cnextcn  21918  symgtgp  21952  tsmssubm  21993  tsmsxplem1  22003  ustfilxp  22063  ustuqtop0  22091  elbl2ps  22241  elbl2  22242  nrginvrcn  22543  nmoix  22580  nmoleub  22582  cncfco  22757  icccvx  22796  iscmet3  23137  rrxmet  23237  ovolfioo  23282  ovolficc  23283  ovolicc2lem4  23334  iunmbl2  23371  dyadmax  23412  mbfsup  23476  mbflimsup  23478  mbflim  23480  itg1addlem4  23511  mbfi1flimlem  23534  itg2monolem1  23562  itg2mono  23565  itg2i1fseqle  23566  itg2i1fseq  23567  itg2addlem  23570  itg2gt0  23572  itg2cnlem1  23573  itgfsum  23638  cnlimc  23697  dvlip2  23803  itgsubst  23857  plyeq0lem  24011  plypf1  24013  dvtaylp  24169  ulmcaulem  24193  ulmcau  24194  ulmcn  24198  ulmdvlem3  24201  mtest  24203  pserulm  24221  pserdvlem2  24227  logdivlt  24412  advlogexp  24446  cxpexp  24459  cxpcl  24465  xrlimcnp  24740  basellem4  24855  logexprlim  24995  dchrsum2  25038  sumdchr2  25040  rpvmasum2  25246  pntrsumbnd2  25301  pntleml  25345  tglineeltr  25571  brbtwn2  25830  colinearalglem4  25834  axeuclidlem  25887  axcontlem8  25896  axcontlem10  25898  grpoidinvlem3  27488  grpoideu  27491  grpoinveu  27501  nmcvcn  27678  nmounbi  27759  blocnilem  27787  ubthlem1  27854  h2hlm  27965  ocsh  28270  brafnmul  28938  kbpj  28943  nmcexi  29013  lnconi  29020  riesz1  29052  mdbr2  29283  mdsl0  29297  mdslmd3i  29319  csmdsymi  29321  atcvatlem  29372  chirredlem1  29377  chirredi  29381  cdj3lem2b  29424  xrge0infss  29653  oduprs  29784  submarchi  29868  madjusmdetlem2  30022  ordtrest2NEWlem  30096  voliune  30420  fsum2dsub  30813  circlemeth  30846  bnj110  31054  cvxsconn  31351  noreson  31938  btwnouttr2  32254  cgrxfr  32287  btwnxfr  32288  lineext  32308  segcon2  32337  brsegle2  32341  seglecgr12im  32342  segletr  32346  broutsideof3  32358  outsideofeu  32363  lineunray  32379  lineelsb2  32380  neibastop3  32482  isbasisrelowllem1  33333  isbasisrelowllem2  33334  unccur  33522  fin2solem  33525  matunitlindflem1  33535  matunitlindflem2  33536  poimirlem4  33543  poimirlem6  33545  poimirlem7  33546  poimirlem22  33561  poimirlem23  33562  poimirlem25  33564  poimirlem26  33565  poimirlem28  33567  poimirlem30  33569  poimirlem31  33570  poimirlem32  33571  poimir  33572  broucube  33573  heicant  33574  mblfinlem3  33578  volsupnfl  33584  itg2addnclem  33591  itg2addnclem2  33592  itg2addnclem3  33593  ftc1anclem1  33615  ftc1anclem5  33619  ftc1anclem6  33620  ftc1anc  33623  unirep  33637  filbcmb  33665  fzmul  33667  fdc  33671  nninfnub  33677  isbnd2  33712  bndss  33715  prdsbnd  33722  prdstotbnd  33723  ismtyres  33737  rrnmet  33758  rrncmslem  33761  rrnequiv  33764  ghomco  33820  grpokerinj  33822  rngonegmn1l  33870  isdrngo2  33887  rngoisocnv  33910  divrngidl  33957  intidl  33958  unichnidl  33960  prnc  33996  isfldidl  33997  cvrexchlem  35023  ps-2  35082  3atnelvolN  35190  dib1dim  36771  dib1dim2  36774  mzpindd  37626  dvdsabsmod0  37871  radcnvrat  38830  expgrowth  38851  fnchoice  39502  infxrbnd2  39898  infleinflem2  39900  xrralrecnnge  39926  limsuppnfdlem  40251  icccncfext  40418  dvnmul  40476  dvnprodlem2  40480  stoweidlem17  40552  stoweidlem30  40565  stoweidlem38  40573  stoweidlem42  40577  stoweidlem44  40579  fourierdlem31  40673  fourierdlem73  40714  fourierdlem74  40715  fourierdlem75  40716  fourierdlem83  40724  fourierdlem94  40735  fourierdlem113  40754  etransclem4  40773  iinhoiicclem  41208  iccvonmbllem  41213  smfsuplem1  41338  mndpsuppss  42477  aacllem  42875
  Copyright terms: Public domain W3C validator