Theorem an32s 665

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 659	. 2 ⊢ (((𝜑 ∧ 𝜒) ∧ 𝜓) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒))
2		an32s.1	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
3	1, 2	sylbi 220	1 ⊢ (((𝜑 ∧ 𝜒) ∧ 𝜓) → 𝜃)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  anass1rs  668  anabss1  679  biadanid  835  wereu2  5652  ordintdif  6409  ordunisssuc  6466  fssres  6741  dffv2  6973  isocnv  7331  f1oiso  7352  f1ocnvfv3  7408  fiunlem  7939  mpof1o2d  8123  onfununi  8330  oev2  8510  oaordi  8533  oaass  8548  omlimcl  8565  odi  8566  omass  8567  oewordri  8580  oelim2  8583  oeoa  8585  oeoe  8587  nnaordi  8606  omabs  8639  eceqoveq  8822  mapxpen  9141  mapdom2  9146  findcard  9158  dif1ennnALT  9247  fimax2g  9256  isfinite2  9268  fimin2g  9469  rankval3b  9808  isf32lem9  10363  fin1a2s  10416  zornn0g  10507  gchen1  10634  gchen2  10635  intwun  10744  suplem2pr  11062  recexsrlem  11112  axpre-sup  11178  axsup  11309  dedekind  11397  recextlem2  11869  divne0  11908  dfinfre  12220  qreccl  13019  xrlttr  13191  xaddf  13276  xrsupsslem  13359  xrinfmsslem  13360  supxr2  13366  supxrunb1  13371  supxrbnd1  13373  supxrbnd2  13374  modid  13957  seqof  14123  cau3lem  15442  lo1bdd2  15611  o1co  15673  rlimcn3  15677  climcn1  15679  climcn2  15680  rlimsqzlem  15736  caucvgb  15767  fsumrlim  15898  fsumo1  15899  ntrivcvg  15986  rplpwr  16648  dvdssq  16657  nn0seqcvgd  16660  lcmgcdlem  16696  isprm6  16805  phiprmpw  16867  pcneg  16966  prmpwdvds  16996  4sqlem19  17055  0ramcl  17115  imasleval  17627  catpropd  17797  funcres2c  17992  initoeu2  18105  oduprs  18388  latdisdlem  18584  acsfiindd  18641  dirtr  18690  chnind  18709  mndpsuppss  18872  mndind  18937  grpinveu  19098  mulgnn0subcl  19210  mulgsubcl  19211  mhmmulg  19238  cycsubm  19330  cycsubgcl  19334  cycsubgss  19335  ghmmulg  19355  odf1  19689  dfod2  19691  gexdvds2  19712  sylow2blem3  19749  frgpup1  19902  iscyggen2  20008  iscyg3  20013  prdsgsum  20108  ringrghm  20455  pwsgprod  20470  dvdsrcl2  20507  crngunit  20519  dvdsrpropd  20557  isdrng3lem2  20915  lss1d  21147  quscrng  21486  ssdifidllem  21547  ssdifidlprm  21549  mulgghm2  21689  frgpcyg  21786  ip0r  21850  isphld  21867  frlmgsum  21985  uvcresum  22006  psdmul  22394  coe1tmmul  22503  mdetdiagid  22822  matunitlindflem1  22901  matunitlindflem2  22902  cpmatmcllem  22943  tgcl  23194  0ntr  23296  innei  23350  neitr  23405  ordtrest2lem  23428  cncnp  23505  cnnei  23507  2ndcdisj  23682  dislly  23723  dissnlocfin  23755  kgenss  23769  ptcnplem  23847  ptcnp  23848  ptcn  23853  cnmpt2k  23914  qtoprest  23943  kqt0lem  23962  isr0  23963  kqreglem1  23967  trfilss  24115  isufil2  24134  ufileu  24145  hausflim  24207  cnextcn  24293  symgtgp  24332  tsmssubm  24369  tsmsxplem1  24379  ustfilxp  24439  ustuqtop0  24466  elbl2ps  24615  elbl2  24616  nrginvrcn  24918  nmoix  24955  nmoleub  24957  cncfco  25135  icccvx  25178  iscmet3  25521  rrxmet  25636  ovolfioo  25695  ovolficc  25696  ovolicc2lem4  25748  iunmbl2  25785  dyadmax  25826  mbfsup  25892  mbflimsup  25894  mbflim  25896  itg1addlem4  25927  mbfi1flimlem  25950  itg2monolem1  25978  itg2mono  25981  itg2i1fseqle  25982  itg2i1fseq  25983  itg2addlem  25986  itg2gt0  25988  itg2cnlem1  25989  itgfsum  26054  cnlimc  26115  dvlip2  26222  itgsubst  26276  plyeq0lem  26436  plypf1  26438  dvtaylp  26606  ulmcaulem  26630  ulmcau  26631  ulmcn  26635  ulmdvlem3  26638  mtest  26640  pserulm  26658  pserdvlem2  26664  logdivlt  26858  advlogexp  26892  cxpexp  26905  cxpcl  26911  xrlimcnp  27205  basellem4  27320  logexprlim  27461  dchrsum2  27504  sumdchr2  27506  rpvmasum2  27748  pntrsumbnd2  27803  pntleml  27847  noreson  27896  z12zsodd  28747  tglineeltr  28978  plngrotlem2  29145  brbtwn2  29362  colinearalglem4  29366  axeuclidlem  29419  axcontlem8  29428  axcontlem10  29430  grpoidinvlem3  30987  grpoideu  30990  grpoinveu  31000  nmcvcn  31176  nmounbi  31257  blocnilem  31285  ubthlem1  31351  h2hlm  31461  ocsh  31764  brafnmul  32432  kbpj  32437  nmcexi  32507  lnconi  32514  riesz1  32546  mdbr2  32777  mdsl0  32791  mdslmd3i  32813  csmdsymi  32815  atcvatlem  32866  chirredlem1  32871  chirredi  32875  cdj3lem2b  32918  xrge0infss  33231  mgcmntco  33434  lmodvslmhm  33490  suppgsumssiun  33512  gsumwrd2dccatlem  33517  submarchi  33626  dvdsruasso  33818  grplsm0l  33832  ssmxidllem  33876  rprmndvdsru  33939  r1plmhm  34019  mplvrpmmhm  34056  mplvrpmrhm  34057  esplyfval1  34083  lindsunlem  34134  lindsun  34135  fldextrspunlsplem  34183  extdgfialglem2  34203  madjusmdetlem2  34338  zarcmplem  34391  ordtrest2NEWlem  34432  voliune  34740  fsum2dsub  35115  circlemeth  35148  bnj110  35367  cvxsconn  35822  btwnouttr2  36602  cgrxfr  36635  btwnxfr  36636  lineext  36656  segcon2  36685  brsegle2  36689  seglecgr12im  36690  segletr  36694  broutsideof3  36706  outsideofeu  36711  lineunray  36727  lineelsb2  36728  nmulrid  36777  neibastop3  36981  ttcmin  37115  mh-inf3f1  37160  bj-imdiridlem  37937  isbasisrelowllem1  38109  isbasisrelowllem2  38110  fvineqsneu  38165  unccur  38357  fin2solem  38360  lindsadd  38367  poimirlem4  38373  poimirlem6  38375  poimirlem7  38376  poimirlem22  38391  poimirlem23  38392  poimirlem25  38394  poimirlem26  38395  poimirlem28  38397  poimirlem30  38399  poimirlem31  38400  poimirlem32  38401  poimir  38402  broucube  38403  heicant  38404  mblfinlem3  38408  volsupnfl  38414  itg2addnclem  38420  itg2addnclem2  38421  itg2addnclem3  38422  ftc1anclem1  38442  ftc1anclem5  38446  ftc1anclem6  38447  ftc1anc  38450  unirep  38464  filbcmb  38490  fzmul  38491  fdc  38495  nninfnub  38501  isbnd2  38533  bndss  38536  prdsbnd  38543  prdstotbnd  38544  ismtyres  38558  rrnmet  38579  rrncmslem  38582  rrnequiv  38585  ghomco  38641  grpokerinj  38643  rngonegmn1l  38691  isdrngo2  38708  rngoisocnv  38731  divrngidl  38778  intidl  38779  unichnidl  38781  prnc  38817  isfldidl  38818  cvrexchlem  40292  ps-2  40351  3atnelvolN  40459  dib1dim  42038  dib1dim2  42041  expeqidd  43200  evlselv  43435  fsuppind  43436  mzpindd  43591  dvdsabsmod0  43828  radcnvrat  45138  expgrowth  45159  modelac8prim  45815  fnchoice  45863  infxrbnd2  46198  infleinflem2  46200  xrralrecnnge  46219  limsuppnfdlem  46529  icccncfext  46715  dvnmul  46771  dvnprodlem2  46775  stoweidlem17  46845  stoweidlem30  46858  stoweidlem38  46866  stoweidlem42  46870  stoweidlem44  46872  fourierdlem31  46966  fourierdlem73  47007  fourierdlem74  47008  fourierdlem75  47009  fourierdlem83  47017  fourierdlem94  47028  fourierdlem113  47047  etransclem4  47066  hoicvr  47376  iinhoiicclem  47501  iccvonmbllem  47506  smfsuplem1  47639  smfsupdmmbllem  47672  smfinfdmmbllem  47676  itsclquadeu  49707  aacllem  50772  veroquadmodzerod  50817