Theorem an32s 652

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

Step	Hyp	Ref	Expression
1		an32 646	. 2 ⊢ (((𝜑 ∧ 𝜒) ∧ 𝜓) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒))
2		an32s.1	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
3	1, 2	sylbi 217	1 ⊢ (((𝜑 ∧ 𝜒) ∧ 𝜓) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  anass1rs  655  anabss1  666  biadanid  823  wereu2  5682  ordintdif  6434  ordunisssuc  6490  fssres  6774  dffv2  7004  isocnv  7350  f1oiso  7371  f1ocnvfv3  7426  fiunlem  7966  onfununi  8381  oev2  8561  oaordi  8584  oaass  8599  omlimcl  8616  odi  8617  omass  8618  oewordri  8630  oelim2  8633  oeoa  8635  oeoe  8637  nnaordi  8656  omabs  8689  eceqoveq  8862  mapxpen  9183  mapdom2  9188  findcard  9203  dif1ennnALT  9311  fimax2g  9322  isfinite2  9334  fimin2g  9537  rankval3b  9866  isf32lem9  10401  fin1a2s  10454  zornn0g  10545  gchen1  10665  gchen2  10666  intwun  10775  suplem2pr  11093  recexsrlem  11143  axpre-sup  11209  axsup  11336  dedekind  11424  recextlem2  11894  divne0  11934  dfinfre  12249  qreccl  13011  xrlttr  13182  xaddf  13266  xrsupsslem  13349  xrinfmsslem  13350  supxr2  13356  supxrunb1  13361  supxrbnd1  13363  supxrbnd2  13364  modid  13936  seqof  14100  cau3lem  15393  lo1bdd2  15560  o1co  15622  rlimcn3  15626  climcn1  15628  climcn2  15629  rlimsqzlem  15685  caucvgb  15716  fsumrlim  15847  fsumo1  15848  ntrivcvg  15933  rplpwr  16595  dvdssq  16604  nn0seqcvgd  16607  lcmgcdlem  16643  isprm6  16751  phiprmpw  16813  pcneg  16912  prmpwdvds  16942  4sqlem19  17001  0ramcl  17061  imasleval  17586  catpropd  17752  funcres2c  17948  initoeu2  18061  oduprs  18346  latdisdlem  18541  acsfiindd  18598  dirtr  18647  mndpsuppss  18778  mndind  18841  grpinveu  18992  mulgnn0subcl  19105  mulgsubcl  19106  mhmmulg  19133  cycsubm  19220  cycsubgcl  19224  cycsubgss  19225  ghmmulg  19246  odf1  19580  dfod2  19582  gexdvds2  19603  sylow2blem3  19640  frgpup1  19793  iscyggen2  19899  iscyg3  19904  prdsgsum  19999  ringrghm  20310  dvdsrcl2  20366  crngunit  20378  dvdsrpropd  20416  lss1d  20961  quscrng  21293  mulgghm2  21487  frgpcyg  21592  ip0r  21655  isphld  21672  frlmgsum  21792  uvcresum  21813  psdmul  22170  coe1tmmul  22280  mdetdiagid  22606  cpmatmcllem  22724  tgcl  22976  0ntr  23079  innei  23133  neitr  23188  ordtrest2lem  23211  cncnp  23288  cnnei  23290  2ndcdisj  23464  dislly  23505  dissnlocfin  23537  kgenss  23551  ptcnplem  23629  ptcnp  23630  ptcn  23635  cnmpt2k  23696  qtoprest  23725  kqt0lem  23744  isr0  23745  kqreglem1  23749  trfilss  23897  isufil2  23916  ufileu  23927  hausflim  23989  cnextcn  24075  symgtgp  24114  tsmssubm  24151  tsmsxplem1  24161  ustfilxp  24221  ustuqtop0  24249  elbl2ps  24399  elbl2  24400  nrginvrcn  24713  nmoix  24750  nmoleub  24752  cncfco  24933  icccvx  24981  iscmet3  25327  rrxmet  25442  ovolfioo  25502  ovolficc  25503  ovolicc2lem4  25555  iunmbl2  25592  dyadmax  25633  mbfsup  25699  mbflimsup  25701  mbflim  25703  itg1addlem4  25734  mbfi1flimlem  25757  itg2monolem1  25785  itg2mono  25788  itg2i1fseqle  25789  itg2i1fseq  25790  itg2addlem  25793  itg2gt0  25795  itg2cnlem1  25796  itgfsum  25862  cnlimc  25923  dvlip2  26034  itgsubst  26090  plyeq0lem  26249  plypf1  26251  dvtaylp  26412  ulmcaulem  26437  ulmcau  26438  ulmcn  26442  ulmdvlem3  26445  mtest  26447  pserulm  26465  pserdvlem2  26472  logdivlt  26663  advlogexp  26697  cxpexp  26710  cxpcl  26716  xrlimcnp  27011  basellem4  27127  logexprlim  27269  dchrsum2  27312  sumdchr2  27314  rpvmasum2  27556  pntrsumbnd2  27611  pntleml  27655  noreson  27705  tglineeltr  28639  brbtwn2  28920  colinearalglem4  28924  axeuclidlem  28977  axcontlem8  28986  axcontlem10  28988  grpoidinvlem3  30525  grpoideu  30528  grpoinveu  30538  nmcvcn  30714  nmounbi  30795  blocnilem  30823  ubthlem1  30889  h2hlm  30999  ocsh  31302  brafnmul  31970  kbpj  31975  nmcexi  32045  lnconi  32052  riesz1  32084  mdbr2  32315  mdsl0  32329  mdslmd3i  32351  csmdsymi  32353  atcvatlem  32404  chirredlem1  32409  chirredi  32413  cdj3lem2b  32456  xrge0infss  32764  mgcmntco  32984  chnind  33001  lmodvslmhm  33053  gsumwrd2dccatlem  33069  submarchi  33193  dvdsruasso  33413  grplsm0l  33431  ssdifidllem  33484  ssdifidlprm  33486  ssmxidllem  33501  rprmndvdsru  33557  r1plmhm  33630  lindsunlem  33675  lindsun  33676  fldextrspunlsplem  33723  madjusmdetlem2  33827  zarcmplem  33880  ordtrest2NEWlem  33921  voliune  34230  fsum2dsub  34622  circlemeth  34655  bnj110  34872  cvxsconn  35248  btwnouttr2  36023  cgrxfr  36056  btwnxfr  36057  lineext  36077  segcon2  36106  brsegle2  36110  seglecgr12im  36111  segletr  36115  broutsideof3  36127  outsideofeu  36132  lineunray  36148  lineelsb2  36149  neibastop3  36363  bj-imdiridlem  37186  isbasisrelowllem1  37356  isbasisrelowllem2  37357  fvineqsneu  37412  unccur  37610  fin2solem  37613  lindsadd  37620  matunitlindflem1  37623  matunitlindflem2  37624  poimirlem4  37631  poimirlem6  37633  poimirlem7  37634  poimirlem22  37649  poimirlem23  37650  poimirlem25  37652  poimirlem26  37653  poimirlem28  37655  poimirlem30  37657  poimirlem31  37658  poimirlem32  37659  poimir  37660  broucube  37661  heicant  37662  mblfinlem3  37666  volsupnfl  37672  itg2addnclem  37678  itg2addnclem2  37679  itg2addnclem3  37680  ftc1anclem1  37700  ftc1anclem5  37704  ftc1anclem6  37705  ftc1anc  37708  unirep  37721  filbcmb  37747  fzmul  37748  fdc  37752  nninfnub  37758  isbnd2  37790  bndss  37793  prdsbnd  37800  prdstotbnd  37801  ismtyres  37815  rrnmet  37836  rrncmslem  37839  rrnequiv  37842  ghomco  37898  grpokerinj  37900  rngonegmn1l  37948  isdrngo2  37965  rngoisocnv  37988  divrngidl  38035  intidl  38036  unichnidl  38038  prnc  38074  isfldidl  38075  cvrexchlem  39421  ps-2  39480  3atnelvolN  39588  dib1dim  41167  dib1dim2  41170  f1o2d2  42274  expeqidd  42360  pwsgprod  42554  evlselv  42597  fsuppind  42600  mzpindd  42757  dvdsabsmod0  42999  radcnvrat  44333  expgrowth  44354  modelac8prim  45009  fnchoice  45034  infxrbnd2  45380  infleinflem2  45382  xrralrecnnge  45401  limsuppnfdlem  45716  icccncfext  45902  dvnmul  45958  dvnprodlem2  45962  stoweidlem17  46032  stoweidlem30  46045  stoweidlem38  46053  stoweidlem42  46057  stoweidlem44  46059  fourierdlem31  46153  fourierdlem73  46194  fourierdlem74  46195  fourierdlem75  46196  fourierdlem83  46204  fourierdlem94  46215  fourierdlem113  46234  etransclem4  46253  iinhoiicclem  46688  iccvonmbllem  46693  smfsuplem1  46826  smfsupdmmbllem  46859  smfinfdmmbllem  46863  itsclquadeu  48698  aacllem  49320