Theorem an32s 651

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 645	. 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  654  anabss1  665  biadanid  822  wereu2  5697  ordintdif  6445  ordunisssuc  6501  fssres  6787  dffv2  7017  isocnv  7366  f1oiso  7387  f1ocnvfv3  7443  fiunlem  7982  onfununi  8397  oev2  8579  oaordi  8602  oaass  8617  omlimcl  8634  odi  8635  omass  8636  oewordri  8648  oelim2  8651  oeoa  8653  oeoe  8655  nnaordi  8674  omabs  8707  eceqoveq  8880  mapxpen  9209  mapdom2  9214  findcard  9229  dif1ennnALT  9339  fimax2g  9350  isfinite2  9362  fimin2g  9566  rankval3b  9895  isf32lem9  10430  fin1a2s  10483  zornn0g  10574  gchen1  10694  gchen2  10695  intwun  10804  suplem2pr  11122  recexsrlem  11172  axpre-sup  11238  axsup  11365  dedekind  11453  recextlem2  11921  divne0  11961  dfinfre  12276  qreccl  13034  xrlttr  13202  xaddf  13286  xrsupsslem  13369  xrinfmsslem  13370  supxr2  13376  supxrunb1  13381  supxrbnd1  13383  supxrbnd2  13384  modid  13947  seqof  14110  cau3lem  15403  lo1bdd2  15570  o1co  15632  rlimcn3  15636  climcn1  15638  climcn2  15639  rlimsqzlem  15697  caucvgb  15728  fsumrlim  15859  fsumo1  15860  ntrivcvg  15945  rplpwr  16605  dvdssq  16614  nn0seqcvgd  16617  lcmgcdlem  16653  isprm6  16761  phiprmpw  16823  pcneg  16921  prmpwdvds  16951  4sqlem19  17010  0ramcl  17070  imasleval  17601  catpropd  17767  funcres2c  17968  initoeu2  18083  latdisdlem  18566  acsfiindd  18623  dirtr  18672  mndind  18863  grpinveu  19014  mulgnn0subcl  19127  mulgsubcl  19128  mhmmulg  19155  cycsubm  19242  cycsubgcl  19246  cycsubgss  19247  ghmmulg  19268  odf1  19604  dfod2  19606  gexdvds2  19627  sylow2blem3  19664  frgpup1  19817  iscyggen2  19923  iscyg3  19928  prdsgsum  20023  ringrghm  20336  dvdsrcl2  20392  crngunit  20404  dvdsrpropd  20442  lss1d  20984  quscrng  21316  mulgghm2  21510  frgpcyg  21615  ip0r  21678  isphld  21695  frlmgsum  21815  uvcresum  21836  psdmul  22193  coe1tmmul  22301  mdetdiagid  22627  cpmatmcllem  22745  tgcl  22997  0ntr  23100  innei  23154  neitr  23209  ordtrest2lem  23232  cncnp  23309  cnnei  23311  2ndcdisj  23485  dislly  23526  dissnlocfin  23558  kgenss  23572  ptcnplem  23650  ptcnp  23651  ptcn  23656  cnmpt2k  23717  qtoprest  23746  kqt0lem  23765  isr0  23766  kqreglem1  23770  trfilss  23918  isufil2  23937  ufileu  23948  hausflim  24010  cnextcn  24096  symgtgp  24135  tsmssubm  24172  tsmsxplem1  24182  ustfilxp  24242  ustuqtop0  24270  elbl2ps  24420  elbl2  24421  nrginvrcn  24734  nmoix  24771  nmoleub  24773  cncfco  24952  icccvx  25000  iscmet3  25346  rrxmet  25461  ovolfioo  25521  ovolficc  25522  ovolicc2lem4  25574  iunmbl2  25611  dyadmax  25652  mbfsup  25718  mbflimsup  25720  mbflim  25722  itg1addlem4  25753  itg1addlem4OLD  25754  mbfi1flimlem  25777  itg2monolem1  25805  itg2mono  25808  itg2i1fseqle  25809  itg2i1fseq  25810  itg2addlem  25813  itg2gt0  25815  itg2cnlem1  25816  itgfsum  25882  cnlimc  25943  dvlip2  26054  itgsubst  26110  plyeq0lem  26269  plypf1  26271  dvtaylp  26430  ulmcaulem  26455  ulmcau  26456  ulmcn  26460  ulmdvlem3  26463  mtest  26465  pserulm  26483  pserdvlem2  26490  logdivlt  26681  advlogexp  26715  cxpexp  26728  cxpcl  26734  xrlimcnp  27029  basellem4  27145  logexprlim  27287  dchrsum2  27330  sumdchr2  27332  rpvmasum2  27574  pntrsumbnd2  27629  pntleml  27673  noreson  27723  tglineeltr  28657  brbtwn2  28938  colinearalglem4  28942  axeuclidlem  28995  axcontlem8  29004  axcontlem10  29006  grpoidinvlem3  30538  grpoideu  30541  grpoinveu  30551  nmcvcn  30727  nmounbi  30808  blocnilem  30836  ubthlem1  30902  h2hlm  31012  ocsh  31315  brafnmul  31983  kbpj  31988  nmcexi  32058  lnconi  32065  riesz1  32097  mdbr2  32328  mdsl0  32342  mdslmd3i  32364  csmdsymi  32366  atcvatlem  32417  chirredlem1  32422  chirredi  32426  cdj3lem2b  32469  xrge0infss  32767  oduprs  32937  mgcmntco  32967  chnind  32983  lmodvslmhm  33033  submarchi  33166  dvdsruasso  33378  grplsm0l  33396  ssdifidllem  33449  ssdifidlprm  33451  ssmxidllem  33466  rprmndvdsru  33522  r1plmhm  33595  lindsunlem  33637  lindsun  33638  madjusmdetlem2  33774  zarcmplem  33827  ordtrest2NEWlem  33868  voliune  34193  fsum2dsub  34584  circlemeth  34617  bnj110  34834  cvxsconn  35211  btwnouttr2  35986  cgrxfr  36019  btwnxfr  36020  lineext  36040  segcon2  36069  brsegle2  36073  seglecgr12im  36074  segletr  36078  broutsideof3  36090  outsideofeu  36095  lineunray  36111  lineelsb2  36112  neibastop3  36328  bj-imdiridlem  37151  isbasisrelowllem1  37321  isbasisrelowllem2  37322  fvineqsneu  37377  unccur  37563  fin2solem  37566  lindsadd  37573  matunitlindflem1  37576  matunitlindflem2  37577  poimirlem4  37584  poimirlem6  37586  poimirlem7  37587  poimirlem22  37602  poimirlem23  37603  poimirlem25  37605  poimirlem26  37606  poimirlem28  37608  poimirlem30  37610  poimirlem31  37611  poimirlem32  37612  poimir  37613  broucube  37614  heicant  37615  mblfinlem3  37619  volsupnfl  37625  itg2addnclem  37631  itg2addnclem2  37632  itg2addnclem3  37633  ftc1anclem1  37653  ftc1anclem5  37657  ftc1anclem6  37658  ftc1anc  37661  unirep  37674  filbcmb  37700  fzmul  37701  fdc  37705  nninfnub  37711  isbnd2  37743  bndss  37746  prdsbnd  37753  prdstotbnd  37754  ismtyres  37768  rrnmet  37789  rrncmslem  37792  rrnequiv  37795  ghomco  37851  grpokerinj  37853  rngonegmn1l  37901  isdrngo2  37918  rngoisocnv  37941  divrngidl  37988  intidl  37989  unichnidl  37991  prnc  38027  isfldidl  38028  cvrexchlem  39376  ps-2  39435  3atnelvolN  39543  dib1dim  41122  dib1dim2  41125  f1o2d2  42228  expeqidd  42312  pwsgprod  42499  evlselv  42542  fsuppind  42545  mzpindd  42702  dvdsabsmod0  42944  radcnvrat  44283  expgrowth  44304  fnchoice  44929  infxrbnd2  45284  infleinflem2  45286  xrralrecnnge  45305  limsuppnfdlem  45622  icccncfext  45808  dvnmul  45864  dvnprodlem2  45868  stoweidlem17  45938  stoweidlem30  45951  stoweidlem38  45959  stoweidlem42  45963  stoweidlem44  45965  fourierdlem31  46059  fourierdlem73  46100  fourierdlem74  46101  fourierdlem75  46102  fourierdlem83  46110  fourierdlem94  46121  fourierdlem113  46140  etransclem4  46159  iinhoiicclem  46594  iccvonmbllem  46599  smfsuplem1  46732  smfsupdmmbllem  46765  smfinfdmmbllem  46769  mndpsuppss  48096  itsclquadeu  48511  aacllem  48895