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

Theorem an32s 648
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 642 . 2 (((𝜑𝜒) ∧ 𝜓) ↔ ((𝜑𝜓) ∧ 𝜒))
2 an32s.1 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
31, 2sylbi 218 1 (((𝜑𝜒) ∧ 𝜓) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396
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 208  df-an 397
This theorem is referenced by:  anass1rs  651  anabss1  662  wereu2  5551  ordintdif  6238  ordunisssuc  6291  fssres  6541  foco  6599  dffv2  6753  isocnv  7075  f1oiso  7096  f1ocnvfv3  7144  fiunlemw  7631  fiunlem  7634  onfununi  7969  oev2  8139  oaordi  8162  oaass  8177  omlimcl  8194  odi  8195  omass  8196  oewordri  8208  oelim2  8211  oeoa  8213  oeoe  8215  nnaordi  8234  omabs  8264  eceqoveq  8392  mapxpen  8672  mapdom2  8677  dif1en  8740  findcard  8746  fimax2g  8753  isfinite2  8765  fimin2g  8950  rankval3b  9244  isf32lem9  9772  fin1a2s  9825  zornn0g  9916  gchen1  10036  gchen2  10037  intwun  10146  suplem2pr  10464  recexsrlem  10514  axpre-sup  10580  axsup  10705  dedekind  10792  recextlem2  11260  divne0  11299  dfinfre  11611  qreccl  12358  xrlttr  12523  xaddf  12607  xrsupsslem  12690  xrinfmsslem  12691  supxr2  12697  supxrunb1  12702  supxrbnd1  12704  supxrbnd2  12705  modid  13254  seqof  13417  cau3lem  14704  lo1bdd2  14871  o1co  14933  rlimcn2  14937  climcn1  14938  climcn2  14939  rlimsqzlem  14995  caucvgb  15026  fsumrlim  15156  fsumo1  15157  ntrivcvg  15243  rplpwr  15897  dvdssq  15901  nn0seqcvgd  15904  lcmgcdlem  15940  isprm6  16048  phiprmpw  16103  pcneg  16200  prmpwdvds  16230  4sqlem19  16289  0ramcl  16349  imasleval  16804  catpropd  16969  funcres2c  17161  initoeu2  17266  acsfiindd  17777  latdisdlem  17789  dirtr  17836  mndind  17975  grpinveu  18068  mulgnn0subcl  18171  mulgsubcl  18172  mhmmulg  18198  cycsubm  18275  cycsubgcl  18279  cycsubgss  18280  ghmmulg  18300  odf1  18609  dfod2  18611  gexdvds2  18630  sylow2blem3  18667  frgpup1  18821  iscyggen2  18920  iscyg3  18925  prdsgsum  19021  ringrghm  19275  dvdsrcl2  19320  crngunit  19332  dvdsrpropd  19366  lss1d  19655  quscrng  19932  coe1tmmul  20362  mulgghm2  20560  frgpcyg  20636  ip0r  20697  isphld  20714  frlmgsum  20832  uvcresum  20853  mdetdiagid  21125  cpmatmcllem  21242  tgcl  21493  0ntr  21595  innei  21649  neitr  21704  ordtrest2lem  21727  cncnp  21804  cnnei  21806  2ndcdisj  21980  dislly  22021  dissnlocfin  22053  kgenss  22067  ptcnplem  22145  ptcnp  22146  ptcn  22151  cnmpt2k  22212  qtoprest  22241  kqt0lem  22260  isr0  22261  kqreglem1  22265  trfilss  22413  isufil2  22432  ufileu  22443  hausflim  22505  cnextcn  22591  symgtgp  22625  tsmssubm  22666  tsmsxplem1  22676  ustfilxp  22736  ustuqtop0  22764  elbl2ps  22914  elbl2  22915  nrginvrcn  23216  nmoix  23253  nmoleub  23255  cncfco  23430  icccvx  23469  iscmet3  23811  rrxmet  23926  ovolfioo  23983  ovolficc  23984  ovolicc2lem4  24036  iunmbl2  24073  dyadmax  24114  mbfsup  24180  mbflimsup  24182  mbflim  24184  itg1addlem4  24215  mbfi1flimlem  24238  itg2monolem1  24266  itg2mono  24269  itg2i1fseqle  24270  itg2i1fseq  24271  itg2addlem  24274  itg2gt0  24276  itg2cnlem1  24277  itgfsum  24342  cnlimc  24401  dvlip2  24507  itgsubst  24561  plyeq0lem  24715  plypf1  24717  dvtaylp  24873  ulmcaulem  24897  ulmcau  24898  ulmcn  24902  ulmdvlem3  24905  mtest  24907  pserulm  24925  pserdvlem2  24931  logdivlt  25117  advlogexp  25151  cxpexp  25164  cxpcl  25170  xrlimcnp  25460  basellem4  25575  logexprlim  25715  dchrsum2  25758  sumdchr2  25760  rpvmasum2  26002  pntrsumbnd2  26057  pntleml  26101  tglineeltr  26331  brbtwn2  26605  colinearalglem4  26609  axeuclidlem  26662  axcontlem8  26671  axcontlem10  26673  grpoidinvlem3  28197  grpoideu  28200  grpoinveu  28210  nmcvcn  28386  nmounbi  28467  blocnilem  28495  ubthlem1  28561  h2hlm  28671  ocsh  28974  brafnmul  29642  kbpj  29647  nmcexi  29717  lnconi  29724  riesz1  29756  mdbr2  29987  mdsl0  30001  mdslmd3i  30023  csmdsymi  30025  atcvatlem  30076  chirredlem1  30081  chirredi  30085  cdj3lem2b  30128  xrge0infss  30397  oduprs  30557  lmodvslmhm  30602  submarchi  30729  lindsunlem  30906  lindsun  30907  madjusmdetlem2  30979  ordtrest2NEWlem  31051  voliune  31374  fsum2dsub  31764  circlemeth  31797  bnj110  32016  cvxsconn  32374  noreson  33051  btwnouttr2  33367  cgrxfr  33400  btwnxfr  33401  lineext  33421  segcon2  33450  brsegle2  33454  seglecgr12im  33455  segletr  33459  broutsideof3  33471  outsideofeu  33476  lineunray  33492  lineelsb2  33493  neibastop3  33594  isbasisrelowllem1  34505  isbasisrelowllem2  34506  fvineqsneu  34561  unccur  34742  fin2solem  34745  lindsadd  34752  matunitlindflem1  34755  matunitlindflem2  34756  poimirlem4  34763  poimirlem6  34765  poimirlem7  34766  poimirlem22  34781  poimirlem23  34782  poimirlem25  34784  poimirlem26  34785  poimirlem28  34787  poimirlem30  34789  poimirlem31  34790  poimirlem32  34791  poimir  34792  broucube  34793  heicant  34794  mblfinlem3  34798  volsupnfl  34804  itg2addnclem  34810  itg2addnclem2  34811  itg2addnclem3  34812  ftc1anclem1  34834  ftc1anclem5  34838  ftc1anclem6  34839  ftc1anc  34842  unirep  34856  filbcmb  34883  fzmul  34884  fdc  34888  nninfnub  34894  isbnd2  34929  bndss  34932  prdsbnd  34939  prdstotbnd  34940  ismtyres  34954  rrnmet  34975  rrncmslem  34978  rrnequiv  34981  ghomco  35037  grpokerinj  35039  rngonegmn1l  35087  isdrngo2  35104  rngoisocnv  35127  divrngidl  35174  intidl  35175  unichnidl  35177  prnc  35213  isfldidl  35214  cvrexchlem  36422  ps-2  36481  3atnelvolN  36589  dib1dim  38168  dib1dim2  38171  mzpindd  39208  dvdsabsmod0  39449  radcnvrat  40511  expgrowth  40532  fnchoice  41151  infxrbnd2  41502  infleinflem2  41504  xrralrecnnge  41527  limsuppnfdlem  41847  icccncfext  42035  dvnmul  42093  dvnprodlem2  42097  stoweidlem17  42168  stoweidlem30  42181  stoweidlem38  42189  stoweidlem42  42193  stoweidlem44  42195  fourierdlem31  42289  fourierdlem73  42330  fourierdlem74  42331  fourierdlem75  42332  fourierdlem83  42340  fourierdlem94  42351  fourierdlem113  42370  etransclem4  42389  iinhoiicclem  42821  iccvonmbllem  42826  smfsuplem1  42951  mndpsuppss  44251  itsclquadeu  44596  aacllem  44734
  Copyright terms: Public domain W3C validator