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

Theorem an32s 881
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 874 . 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  884  anabss1  890  wereu2  5263  ordintdif  5935  ordunisssuc  5991  fssres  6231  foco  6287  dffv2  6434  isocnv  6744  f1oiso  6765  f1ocnvfv3  6810  fun11iun  7292  onfununi  7608  oev2  7774  oaordi  7797  oaass  7812  omlimcl  7829  odi  7830  omass  7831  oewordri  7843  oelim2  7846  oeoa  7848  oeoe  7850  nnaordi  7869  omabs  7898  eceqoveq  8021  mapxpen  8293  mapdom2  8298  dif1en  8360  findcard  8366  fimax2g  8373  isfinite2  8385  fimin2g  8570  rankval3b  8864  isf32lem9  9395  fin1a2s  9448  zornn0g  9539  gchen1  9659  gchen2  9660  intwun  9769  suplem2pr  10087  recexsrlem  10136  axpre-sup  10202  axsup  10325  dedekind  10412  recextlem2  10870  divne0  10909  dfinfre  11216  qreccl  12021  xrlttr  12186  xaddf  12268  xrsupsslem  12350  xrinfmsslem  12351  supxr2  12357  supxrunb1  12362  supxrbnd1  12364  supxrbnd2  12365  modid  12909  seqof  13072  cau3lem  14313  lo1bdd2  14474  o1co  14536  rlimcn2  14540  climcn1  14541  climcn2  14542  rlimsqzlem  14598  caucvgb  14629  fsumrlim  14762  fsumo1  14763  ntrivcvg  14848  rplpwr  15498  dvdssq  15502  nn0seqcvgd  15505  lcmgcdlem  15541  isprm6  15648  phiprmpw  15703  pcneg  15800  prmpwdvds  15830  4sqlem19  15889  0ramcl  15949  imasleval  16423  catpropd  16590  funcres2c  16782  initoeu2  16887  acsfiindd  17398  latdisdlem  17410  dirtr  17457  mrcmndind  17587  grpinveu  17677  mulgnn0subcl  17775  mulgsubcl  17776  mhmmulg  17804  cycsubgcl  17841  cycsubgss  17842  ghmmulg  17893  odf1  18199  dfod2  18201  gexdvds2  18220  sylow2blem3  18257  frgpup1  18408  iscyggen2  18503  iscyg3  18508  prdsgsum  18597  ringrghm  18825  dvdsrcl2  18870  crngunit  18882  dvdsrpropd  18916  lss1d  19185  quscrng  19462  coe1tmmul  19869  mulgghm2  20067  frgpcyg  20144  ip0r  20204  isphld  20221  frlmgsum  20333  uvcresum  20354  mdetdiagid  20628  cpmatmcllem  20745  tgcl  20995  0ntr  21097  innei  21151  neitr  21206  ordtrest2lem  21229  cncnp  21306  cnnei  21308  2ndcdisj  21481  dislly  21522  dissnlocfin  21554  kgenss  21568  ptcnplem  21646  ptcnp  21647  ptcn  21652  cnmpt2k  21713  qtoprest  21742  kqt0lem  21761  isr0  21762  kqreglem1  21766  trfilss  21914  isufil2  21933  ufileu  21944  hausflim  22006  cnextcn  22092  symgtgp  22126  tsmssubm  22167  tsmsxplem1  22177  ustfilxp  22237  ustuqtop0  22265  elbl2ps  22415  elbl2  22416  nrginvrcn  22717  nmoix  22754  nmoleub  22756  cncfco  22931  icccvx  22970  iscmet3  23311  rrxmet  23411  ovolfioo  23456  ovolficc  23457  ovolicc2lem4  23508  iunmbl2  23545  dyadmax  23586  mbfsup  23650  mbflimsup  23652  mbflim  23654  itg1addlem4  23685  mbfi1flimlem  23708  itg2monolem1  23736  itg2mono  23739  itg2i1fseqle  23740  itg2i1fseq  23741  itg2addlem  23744  itg2gt0  23746  itg2cnlem1  23747  itgfsum  23812  cnlimc  23871  dvlip2  23977  itgsubst  24031  plyeq0lem  24185  plypf1  24187  dvtaylp  24343  ulmcaulem  24367  ulmcau  24368  ulmcn  24372  ulmdvlem3  24375  mtest  24377  pserulm  24395  pserdvlem2  24401  logdivlt  24587  advlogexp  24621  cxpexp  24634  cxpcl  24640  xrlimcnp  24915  basellem4  25030  logexprlim  25170  dchrsum2  25213  sumdchr2  25215  rpvmasum2  25421  pntrsumbnd2  25476  pntleml  25520  tglineeltr  25746  brbtwn2  26005  colinearalglem4  26009  axeuclidlem  26062  axcontlem8  26071  axcontlem10  26073  grpoidinvlem3  27690  grpoideu  27693  grpoinveu  27703  nmcvcn  27880  nmounbi  27961  blocnilem  27989  ubthlem1  28056  h2hlm  28167  ocsh  28472  brafnmul  29140  kbpj  29145  nmcexi  29215  lnconi  29222  riesz1  29254  mdbr2  29485  mdsl0  29499  mdslmd3i  29521  csmdsymi  29523  atcvatlem  29574  chirredlem1  29579  chirredi  29583  cdj3lem2b  29626  xrge0infss  29855  oduprs  29986  submarchi  30070  madjusmdetlem2  30224  ordtrest2NEWlem  30298  voliune  30622  fsum2dsub  31015  circlemeth  31048  bnj110  31256  cvxsconn  31553  noreson  32140  btwnouttr2  32456  cgrxfr  32489  btwnxfr  32490  lineext  32510  segcon2  32539  brsegle2  32543  seglecgr12im  32544  segletr  32548  broutsideof3  32560  outsideofeu  32565  lineunray  32581  lineelsb2  32582  neibastop3  32684  isbasisrelowllem1  33532  isbasisrelowllem2  33533  unccur  33723  fin2solem  33726  matunitlindflem1  33736  matunitlindflem2  33737  poimirlem4  33744  poimirlem6  33746  poimirlem7  33747  poimirlem22  33762  poimirlem23  33763  poimirlem25  33765  poimirlem26  33766  poimirlem28  33768  poimirlem30  33770  poimirlem31  33771  poimirlem32  33772  poimir  33773  broucube  33774  heicant  33775  mblfinlem3  33779  volsupnfl  33785  itg2addnclem  33792  itg2addnclem2  33793  itg2addnclem3  33794  ftc1anclem1  33816  ftc1anclem5  33820  ftc1anclem6  33821  ftc1anc  33824  unirep  33838  filbcmb  33866  fzmul  33868  fdc  33872  nninfnub  33878  isbnd2  33913  bndss  33916  prdsbnd  33923  prdstotbnd  33924  ismtyres  33938  rrnmet  33959  rrncmslem  33962  rrnequiv  33965  ghomco  34021  grpokerinj  34023  rngonegmn1l  34071  isdrngo2  34088  rngoisocnv  34111  divrngidl  34158  intidl  34159  unichnidl  34161  prnc  34197  isfldidl  34198  cvrexchlem  35226  ps-2  35285  3atnelvolN  35393  dib1dim  36974  dib1dim2  36977  mzpindd  37829  dvdsabsmod0  38074  radcnvrat  39033  expgrowth  39054  fnchoice  39705  infxrbnd2  40101  infleinflem2  40103  xrralrecnnge  40129  limsuppnfdlem  40454  icccncfext  40621  dvnmul  40679  dvnprodlem2  40683  stoweidlem17  40755  stoweidlem30  40768  stoweidlem38  40776  stoweidlem42  40780  stoweidlem44  40782  fourierdlem31  40876  fourierdlem73  40917  fourierdlem74  40918  fourierdlem75  40919  fourierdlem83  40927  fourierdlem94  40938  fourierdlem113  40957  etransclem4  40976  iinhoiicclem  41411  iccvonmbllem  41416  smfsuplem1  41541  mndpsuppss  42680  aacllem  43078
  Copyright terms: Public domain W3C validator