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  5545  ordintdif  6233  ordunisssuc  6286  fssres  6537  foco  6595  dffv2  6749  isocnv  7072  f1oiso  7093  f1ocnvfv3  7141  fiunlem  7632  onfununi  7967  oev2  8137  oaordi  8161  oaass  8176  omlimcl  8193  odi  8194  omass  8195  oewordri  8207  oelim2  8210  oeoa  8212  oeoe  8214  nnaordi  8233  omabs  8263  eceqoveq  8391  mapxpen  8671  mapdom2  8676  dif1en  8739  findcard  8745  fimax2g  8752  isfinite2  8764  fimin2g  8949  rankval3b  9243  isf32lem9  9771  fin1a2s  9824  zornn0g  9915  gchen1  10035  gchen2  10036  intwun  10145  suplem2pr  10463  recexsrlem  10513  axpre-sup  10579  axsup  10704  dedekind  10791  recextlem2  11259  divne0  11298  dfinfre  11610  qreccl  12356  xrlttr  12521  xaddf  12605  xrsupsslem  12688  xrinfmsslem  12689  supxr2  12695  supxrunb1  12700  supxrbnd1  12702  supxrbnd2  12703  modid  13252  seqof  13415  cau3lem  14702  lo1bdd2  14869  o1co  14931  rlimcn2  14935  climcn1  14936  climcn2  14937  rlimsqzlem  14993  caucvgb  15024  fsumrlim  15154  fsumo1  15155  ntrivcvg  15241  rplpwr  15895  dvdssq  15899  nn0seqcvgd  15902  lcmgcdlem  15938  isprm6  16046  phiprmpw  16101  pcneg  16198  prmpwdvds  16228  4sqlem19  16287  0ramcl  16347  imasleval  16802  catpropd  16967  funcres2c  17159  initoeu2  17264  acsfiindd  17775  latdisdlem  17787  dirtr  17834  mndind  17980  grpinveu  18076  mulgnn0subcl  18179  mulgsubcl  18180  mhmmulg  18206  cycsubm  18283  cycsubgcl  18287  cycsubgss  18288  ghmmulg  18308  odf1  18618  dfod2  18620  gexdvds2  18639  sylow2blem3  18676  frgpup1  18830  iscyggen2  18929  iscyg3  18934  prdsgsum  19030  ringrghm  19284  dvdsrcl2  19329  crngunit  19341  dvdsrpropd  19375  lss1d  19664  quscrng  19941  coe1tmmul  20373  mulgghm2  20572  frgpcyg  20648  ip0r  20709  isphld  20726  frlmgsum  20844  uvcresum  20865  mdetdiagid  21137  cpmatmcllem  21254  tgcl  21505  0ntr  21607  innei  21661  neitr  21716  ordtrest2lem  21739  cncnp  21816  cnnei  21818  2ndcdisj  21992  dislly  22033  dissnlocfin  22065  kgenss  22079  ptcnplem  22157  ptcnp  22158  ptcn  22163  cnmpt2k  22224  qtoprest  22253  kqt0lem  22272  isr0  22273  kqreglem1  22277  trfilss  22425  isufil2  22444  ufileu  22455  hausflim  22517  cnextcn  22603  symgtgp  22637  tsmssubm  22678  tsmsxplem1  22688  ustfilxp  22748  ustuqtop0  22776  elbl2ps  22926  elbl2  22927  nrginvrcn  23228  nmoix  23265  nmoleub  23267  cncfco  23442  icccvx  23481  iscmet3  23823  rrxmet  23938  ovolfioo  23995  ovolficc  23996  ovolicc2lem4  24048  iunmbl2  24085  dyadmax  24126  mbfsup  24192  mbflimsup  24194  mbflim  24196  itg1addlem4  24227  mbfi1flimlem  24250  itg2monolem1  24278  itg2mono  24281  itg2i1fseqle  24282  itg2i1fseq  24283  itg2addlem  24286  itg2gt0  24288  itg2cnlem1  24289  itgfsum  24354  cnlimc  24413  dvlip2  24519  itgsubst  24573  plyeq0lem  24727  plypf1  24729  dvtaylp  24885  ulmcaulem  24909  ulmcau  24910  ulmcn  24914  ulmdvlem3  24917  mtest  24919  pserulm  24937  pserdvlem2  24943  logdivlt  25131  advlogexp  25165  cxpexp  25178  cxpcl  25184  xrlimcnp  25473  basellem4  25588  logexprlim  25728  dchrsum2  25771  sumdchr2  25773  rpvmasum2  26015  pntrsumbnd2  26070  pntleml  26114  tglineeltr  26344  brbtwn2  26618  colinearalglem4  26622  axeuclidlem  26675  axcontlem8  26684  axcontlem10  26686  grpoidinvlem3  28210  grpoideu  28213  grpoinveu  28223  nmcvcn  28399  nmounbi  28480  blocnilem  28508  ubthlem1  28574  h2hlm  28684  ocsh  28987  brafnmul  29655  kbpj  29660  nmcexi  29730  lnconi  29737  riesz1  29769  mdbr2  30000  mdsl0  30014  mdslmd3i  30036  csmdsymi  30038  atcvatlem  30089  chirredlem1  30094  chirredi  30098  cdj3lem2b  30141  xrge0infss  30410  oduprs  30570  lmodvslmhm  30615  submarchi  30742  lindsunlem  30919  lindsun  30920  madjusmdetlem2  30992  ordtrest2NEWlem  31064  voliune  31387  fsum2dsub  31777  circlemeth  31810  bnj110  32029  cvxsconn  32387  noreson  33064  btwnouttr2  33380  cgrxfr  33413  btwnxfr  33414  lineext  33434  segcon2  33463  brsegle2  33467  seglecgr12im  33468  segletr  33472  broutsideof3  33484  outsideofeu  33489  lineunray  33505  lineelsb2  33506  neibastop3  33607  isbasisrelowllem1  34518  isbasisrelowllem2  34519  fvineqsneu  34574  unccur  34756  fin2solem  34759  lindsadd  34766  matunitlindflem1  34769  matunitlindflem2  34770  poimirlem4  34777  poimirlem6  34779  poimirlem7  34780  poimirlem22  34795  poimirlem23  34796  poimirlem25  34798  poimirlem26  34799  poimirlem28  34801  poimirlem30  34803  poimirlem31  34804  poimirlem32  34805  poimir  34806  broucube  34807  heicant  34808  mblfinlem3  34812  volsupnfl  34818  itg2addnclem  34824  itg2addnclem2  34825  itg2addnclem3  34826  ftc1anclem1  34848  ftc1anclem5  34852  ftc1anclem6  34853  ftc1anc  34856  unirep  34869  filbcmb  34896  fzmul  34897  fdc  34901  nninfnub  34907  isbnd2  34942  bndss  34945  prdsbnd  34952  prdstotbnd  34953  ismtyres  34967  rrnmet  34988  rrncmslem  34991  rrnequiv  34994  ghomco  35050  grpokerinj  35052  rngonegmn1l  35100  isdrngo2  35117  rngoisocnv  35140  divrngidl  35187  intidl  35188  unichnidl  35190  prnc  35226  isfldidl  35227  cvrexchlem  36435  ps-2  36494  3atnelvolN  36602  dib1dim  38181  dib1dim2  38184  mzpindd  39221  dvdsabsmod0  39462  radcnvrat  40523  expgrowth  40544  fnchoice  41163  infxrbnd2  41513  infleinflem2  41515  xrralrecnnge  41538  limsuppnfdlem  41858  icccncfext  42046  dvnmul  42104  dvnprodlem2  42108  stoweidlem17  42179  stoweidlem30  42192  stoweidlem38  42200  stoweidlem42  42204  stoweidlem44  42206  fourierdlem31  42300  fourierdlem73  42341  fourierdlem74  42342  fourierdlem75  42343  fourierdlem83  42351  fourierdlem94  42362  fourierdlem113  42381  etransclem4  42400  iinhoiicclem  42832  iccvonmbllem  42837  smfsuplem1  42962  mndpsuppss  44347  itsclquadeu  44692  aacllem  44830
  Copyright terms: Public domain W3C validator