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

Theorem an32s 634
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 628 . 2 (((𝜑𝜒) ∧ 𝜓) ↔ ((𝜑𝜓) ∧ 𝜒))
2 an32s.1 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
31, 2sylbi 208 1 (((𝜑𝜒) ∧ 𝜓) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384
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 198  df-an 385
This theorem is referenced by:  anass1rs  637  anabss1  648  wereu2  5308  ordintdif  5986  ordunisssuc  6039  fssres  6281  foco  6337  dffv2  6488  isocnv  6800  f1oiso  6821  f1ocnvfv3  6866  fun11iun  7352  onfununi  7670  oev2  7836  oaordi  7859  oaass  7874  omlimcl  7891  odi  7892  omass  7893  oewordri  7905  oelim2  7908  oeoa  7910  oeoe  7912  nnaordi  7931  omabs  7960  eceqoveq  8084  mapxpen  8361  mapdom2  8366  dif1en  8428  findcard  8434  fimax2g  8441  isfinite2  8453  fimin2g  8638  rankval3b  8932  isf32lem9  9464  fin1a2s  9517  zornn0g  9608  gchen1  9728  gchen2  9729  intwun  9838  suplem2pr  10156  recexsrlem  10205  axpre-sup  10271  axsup  10394  dedekind  10481  recextlem2  10939  divne0  10978  dfinfre  11285  qreccl  12023  xrlttr  12185  xaddf  12269  xrsupsslem  12351  xrinfmsslem  12352  supxr2  12358  supxrunb1  12363  supxrbnd1  12365  supxrbnd2  12366  modid  12915  seqof  13077  cau3lem  14313  lo1bdd2  14474  o1co  14536  rlimcn2  14540  climcn1  14541  climcn2  14542  rlimsqzlem  14598  caucvgb  14629  fsumrlim  14761  fsumo1  14762  ntrivcvg  14846  rplpwr  15491  dvdssq  15495  nn0seqcvgd  15498  lcmgcdlem  15534  isprm6  15639  phiprmpw  15694  pcneg  15791  prmpwdvds  15821  4sqlem19  15880  0ramcl  15940  imasleval  16402  catpropd  16569  funcres2c  16761  initoeu2  16866  acsfiindd  17378  latdisdlem  17390  dirtr  17437  mrcmndind  17567  grpinveu  17657  mulgnn0subcl  17755  mulgsubcl  17756  mhmmulg  17781  cycsubgcl  17818  cycsubgss  17819  ghmmulg  17870  odf1  18176  dfod2  18178  gexdvds2  18197  sylow2blem3  18234  frgpup1  18385  iscyggen2  18480  iscyg3  18485  prdsgsum  18574  ringrghm  18803  dvdsrcl2  18848  crngunit  18860  dvdsrpropd  18894  lss1d  19166  quscrng  19445  coe1tmmul  19851  mulgghm2  20049  frgpcyg  20125  ip0r  20188  isphld  20205  frlmgsum  20318  uvcresum  20339  mdetdiagid  20614  cpmatmcllem  20733  tgcl  20984  0ntr  21086  innei  21140  neitr  21195  ordtrest2lem  21218  cncnp  21295  cnnei  21297  2ndcdisj  21470  dislly  21511  dissnlocfin  21543  kgenss  21557  ptcnplem  21635  ptcnp  21636  ptcn  21641  cnmpt2k  21702  qtoprest  21731  kqt0lem  21750  isr0  21751  kqreglem1  21755  trfilss  21903  isufil2  21922  ufileu  21933  hausflim  21995  cnextcn  22081  symgtgp  22115  tsmssubm  22156  tsmsxplem1  22166  ustfilxp  22226  ustuqtop0  22254  elbl2ps  22404  elbl2  22405  nrginvrcn  22706  nmoix  22743  nmoleub  22745  cncfco  22920  icccvx  22959  iscmet3  23301  rrxmet  23402  ovolfioo  23447  ovolficc  23448  ovolicc2lem4  23500  iunmbl2  23537  dyadmax  23578  mbfsup  23644  mbflimsup  23646  mbflim  23648  itg1addlem4  23679  mbfi1flimlem  23702  itg2monolem1  23730  itg2mono  23733  itg2i1fseqle  23734  itg2i1fseq  23735  itg2addlem  23738  itg2gt0  23740  itg2cnlem1  23741  itgfsum  23806  cnlimc  23865  dvlip2  23971  itgsubst  24025  plyeq0lem  24179  plypf1  24181  dvtaylp  24337  ulmcaulem  24361  ulmcau  24362  ulmcn  24366  ulmdvlem3  24369  mtest  24371  pserulm  24389  pserdvlem2  24395  logdivlt  24580  advlogexp  24614  cxpexp  24627  cxpcl  24633  xrlimcnp  24908  basellem4  25023  logexprlim  25163  dchrsum2  25206  sumdchr2  25208  rpvmasum2  25414  pntrsumbnd2  25469  pntleml  25513  tglineeltr  25739  brbtwn2  25998  colinearalglem4  26002  axeuclidlem  26055  axcontlem8  26064  axcontlem10  26066  grpoidinvlem3  27688  grpoideu  27691  grpoinveu  27701  nmcvcn  27877  nmounbi  27958  blocnilem  27986  ubthlem1  28053  h2hlm  28164  ocsh  28469  brafnmul  29137  kbpj  29142  nmcexi  29212  lnconi  29219  riesz1  29251  mdbr2  29482  mdsl0  29496  mdslmd3i  29518  csmdsymi  29520  atcvatlem  29571  chirredlem1  29576  chirredi  29580  cdj3lem2b  29623  xrge0infss  29851  oduprs  29980  submarchi  30064  madjusmdetlem2  30218  ordtrest2NEWlem  30292  voliune  30616  fsum2dsub  31009  circlemeth  31042  bnj110  31249  cvxsconn  31546  noreson  32132  btwnouttr2  32448  cgrxfr  32481  btwnxfr  32482  lineext  32502  segcon2  32531  brsegle2  32535  seglecgr12im  32536  segletr  32540  broutsideof3  32552  outsideofeu  32557  lineunray  32573  lineelsb2  32574  neibastop3  32676  isbasisrelowllem1  33517  isbasisrelowllem2  33518  unccur  33703  fin2solem  33706  matunitlindflem1  33716  matunitlindflem2  33717  poimirlem4  33724  poimirlem6  33726  poimirlem7  33727  poimirlem22  33742  poimirlem23  33743  poimirlem25  33745  poimirlem26  33746  poimirlem28  33748  poimirlem30  33750  poimirlem31  33751  poimirlem32  33752  poimir  33753  broucube  33754  heicant  33755  mblfinlem3  33759  volsupnfl  33765  itg2addnclem  33771  itg2addnclem2  33772  itg2addnclem3  33773  ftc1anclem1  33795  ftc1anclem5  33799  ftc1anclem6  33800  ftc1anc  33803  unirep  33817  filbcmb  33845  fzmul  33846  fdc  33850  nninfnub  33856  isbnd2  33891  bndss  33894  prdsbnd  33901  prdstotbnd  33902  ismtyres  33916  rrnmet  33937  rrncmslem  33940  rrnequiv  33943  ghomco  33999  grpokerinj  34001  rngonegmn1l  34049  isdrngo2  34066  rngoisocnv  34089  divrngidl  34136  intidl  34137  unichnidl  34139  prnc  34175  isfldidl  34176  cvrexchlem  35197  ps-2  35256  3atnelvolN  35364  dib1dim  36943  dib1dim2  36946  mzpindd  37808  dvdsabsmod0  38052  radcnvrat  39010  expgrowth  39031  fnchoice  39679  infxrbnd2  40062  infleinflem2  40064  xrralrecnnge  40089  limsuppnfdlem  40410  icccncfext  40577  dvnmul  40635  dvnprodlem2  40639  stoweidlem17  40710  stoweidlem30  40723  stoweidlem38  40731  stoweidlem42  40735  stoweidlem44  40737  fourierdlem31  40831  fourierdlem73  40872  fourierdlem74  40873  fourierdlem75  40874  fourierdlem83  40882  fourierdlem94  40893  fourierdlem113  40912  etransclem4  40931  iinhoiicclem  41366  iccvonmbllem  41371  smfsuplem1  41496  mndpsuppss  42717  aacllem  43115
  Copyright terms: Public domain W3C validator