Theorem an32s 842

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

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 196  df-an 385

This theorem is referenced by:  anass1rs  845  anabss1  851  wereu2  5035  ordintdif  5691  ordunisssuc  5747  fssres  5983  foco  6038  dffv2  6181  isocnv  6480  f1oiso  6501  f1ocnvfv3  6545  fun11iun  7019  onfununi  7325  oev2  7490  oaordi  7513  oaass  7528  omlimcl  7545  odi  7546  omass  7547  oewordri  7559  oelim2  7562  oeoa  7564  oeoe  7566  nnaordi  7585  omabs  7614  eceqoveq  7740  mapxpen  8011  mapdom2  8016  dif1en  8078  findcard  8084  fimax2g  8091  isfinite2  8103  fimin2g  8286  rankval3b  8572  isf32lem9  9066  fin1a2s  9119  zornn0g  9210  gchen1  9326  gchen2  9327  intwun  9436  suplem2pr  9754  recexsrlem  9803  axpre-sup  9869  axsup  9992  dedekind  10079  recextlem2  10537  divne0  10576  dfinfre  10881  qreccl  11684  xrlttr  11849  xaddf  11929  xrsupsslem  12009  xrinfmsslem  12010  supxr2  12016  supxrunb1  12021  supxrbnd1  12023  supxrbnd2  12024  modid  12557  seqof  12720  cau3lem  13942  lo1bdd2  14103  o1co  14165  rlimcn2  14169  climcn1  14170  climcn2  14171  rlimsqzlem  14227  caucvgb  14258  fsumrlim  14384  fsumo1  14385  ntrivcvg  14468  rplpwr  15114  dvdssq  15118  nn0seqcvgd  15121  lcmgcdlem  15157  isprm2lem  15232  isprm6  15264  phiprmpw  15319  pcneg  15416  prmpwdvds  15446  4sqlem19  15505  0ramcl  15565  imasleval  16024  catpropd  16192  funcres2c  16384  initoeu2  16489  acsfiindd  17000  latdisdlem  17012  dirtr  17059  mrcmndind  17189  grpinveu  17279  mulgnn0subcl  17377  mulgsubcl  17378  mhmmulg  17406  cycsubgcl  17443  cycsubgss  17444  ghmmulg  17495  odf1  17802  dfod2  17804  gexdvds2  17823  sylow2blem3  17860  frgpup1  18011  iscyggen2  18106  iscyg3  18111  prdsgsum  18200  ringrghm  18428  dvdsrcl2  18473  crngunit  18485  dvdsrpropd  18519  lss1d  18784  quscrng  19061  coe1tmmul  19468  mulgghm2  19664  frgpcyg  19741  ip0r  19801  isphld  19818  frlmgsum  19930  uvcresum  19951  mdetdiagid  20225  cpmatmcllem  20342  tgcl  20584  0ntr  20685  innei  20739  neitr  20794  ordtrest2lem  20817  cncnp  20894  cnnei  20896  2ndcdisj  21069  dislly  21110  dissnlocfin  21142  kgenss  21156  ptcnplem  21234  ptcnp  21235  ptcn  21240  cnmpt2k  21301  qtoprest  21330  kqt0lem  21349  isr0  21350  kqreglem1  21354  trfilss  21503  isufil2  21522  ufileu  21533  hausflim  21595  cnextcn  21681  symgtgp  21715  tsmssubm  21756  tsmsxplem1  21766  ustfilxp  21826  ustuqtop0  21854  elbl2ps  22004  elbl2  22005  nrginvrcn  22306  nmoix  22343  nmoleub  22345  cncfco  22518  icccvx  22557  iscmet3  22899  rrxmet  22999  ovolfioo  23043  ovolficc  23044  ovolicc2lem4  23095  iunmbl2  23132  dyadmax  23172  mbfsup  23237  mbflimsup  23239  mbflim  23241  itg1addlem4  23272  mbfi1flimlem  23295  itg2monolem1  23323  itg2mono  23326  itg2i1fseqle  23327  itg2i1fseq  23328  itg2addlem  23331  itg2gt0  23333  itg2cnlem1  23334  itgfsum  23399  cnlimc  23458  dvlip2  23562  itgsubst  23616  plyeq0lem  23770  plypf1  23772  dvtaylp  23928  ulmcaulem  23952  ulmcau  23953  ulmcn  23957  ulmdvlem3  23960  mtest  23962  pserulm  23980  pserdvlem2  23986  logdivlt  24171  advlogexp  24201  cxpexp  24214  cxpcl  24220  xrlimcnp  24495  basellem4  24610  logexprlim  24750  dchrsum2  24793  sumdchr2  24795  rpvmasum2  25001  pntrsumbnd2  25056  pntleml  25100  tglineeltr  25326  brbtwn2  25585  colinearalglem4  25589  axeuclidlem  25642  axcontlem8  25651  axcontlem10  25653  clwwisshclww  26335  grpoidinvlem3  26744  grpoideu  26747  grpoinveu  26757  nmcvcn  26934  nmounbi  27015  blocnilem  27043  ubthlem1  27110  h2hlm  27221  ocsh  27526  brafnmul  28194  kbpj  28199  nmcexi  28269  lnconi  28276  riesz1  28308  mdbr2  28539  mdsl0  28553  mdslmd3i  28575  csmdsymi  28577  atcvatlem  28628  chirredlem1  28633  chirredi  28637  cdj3lem2b  28680  xrge0infss  28915  oduprs  28987  submarchi  29071  madjusmdetlem2  29222  ordtrest2NEWlem  29296  voliune  29619  bnj110  30182  cvxscon  30479  noreson  31057  btwnouttr2  31299  cgrxfr  31332  btwnxfr  31333  lineext  31353  segcon2  31382  brsegle2  31386  seglecgr12im  31387  segletr  31391  broutsideof3  31403  outsideofeu  31408  lineunray  31424  lineelsb2  31425  neibastop3  31527  isbasisrelowllem1  32379  isbasisrelowllem2  32380  unccur  32562  fin2solem  32565  matunitlindflem1  32575  matunitlindflem2  32576  poimirlem4  32583  poimirlem6  32585  poimirlem7  32586  poimirlem22  32601  poimirlem23  32602  poimirlem25  32604  poimirlem26  32605  poimirlem28  32607  poimirlem30  32609  poimirlem31  32610  poimirlem32  32611  poimir  32612  broucube  32613  heicant  32614  mblfinlem3  32618  volsupnfl  32624  itg2addnclem  32631  itg2addnclem2  32632  itg2addnclem3  32633  ftc1anclem1  32655  ftc1anclem5  32659  ftc1anclem6  32660  ftc1anc  32663  unirep  32677  filbcmb  32705  fzmul  32707  fdc  32711  nninfnub  32717  isbnd2  32752  bndss  32755  prdsbnd  32762  prdstotbnd  32763  ismtyres  32777  rrnmet  32798  rrncmslem  32801  rrnequiv  32804  ghomco  32860  grpokerinj  32862  rngonegmn1l  32910  isdrngo2  32927  rngoisocnv  32950  divrngidl  32997  intidl  32998  unichnidl  33000  prnc  33036  isfldidl  33037  cvrexchlem  33723  ps-2  33782  3atnelvolN  33890  dib1dim  35472  dib1dim2  35475  mzpindd  36327  dvdsabsmod0  36572  radcnvrat  37535  expgrowth  37556  fnchoice  38211  infxrbnd2  38526  infleinflem2  38528  xrralrecnnge  38554  icccncfext  38773  dvnmul  38833  dvnprodlem2  38837  stoweidlem17  38910  stoweidlem30  38923  stoweidlem38  38931  stoweidlem42  38935  stoweidlem44  38937  fourierdlem31  39031  fourierdlem73  39072  fourierdlem74  39073  fourierdlem75  39074  fourierdlem83  39082  fourierdlem94  39093  fourierdlem113  39112  etransclem4  39131  iinhoiicclem  39564  iccvonmbllem  39569  mndpsuppss  41946  aacllem  42356