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  822  wereu2  5608  ordintdif  6352  ordunisssuc  6409  fssres  6684  dffv2  6912  isocnv  7259  f1oiso  7280  f1ocnvfv3  7336  fiunlem  7869  onfununi  8256  oev2  8433  oaordi  8456  oaass  8471  omlimcl  8488  odi  8489  omass  8490  oewordri  8502  oelim2  8505  oeoa  8507  oeoe  8509  nnaordi  8528  omabs  8561  eceqoveq  8741  mapxpen  9051  mapdom2  9056  findcard  9068  dif1ennnALT  9156  fimax2g  9165  isfinite2  9177  fimin2g  9378  rankval3b  9714  isf32lem9  10247  fin1a2s  10300  zornn0g  10391  gchen1  10511  gchen2  10512  intwun  10621  suplem2pr  10939  recexsrlem  10989  axpre-sup  11055  axsup  11183  dedekind  11271  recextlem2  11743  divne0  11783  dfinfre  12098  qreccl  12862  xrlttr  13034  xaddf  13118  xrsupsslem  13201  xrinfmsslem  13202  supxr2  13208  supxrunb1  13213  supxrbnd1  13215  supxrbnd2  13216  modid  13795  seqof  13961  cau3lem  15257  lo1bdd2  15426  o1co  15488  rlimcn3  15492  climcn1  15494  climcn2  15495  rlimsqzlem  15551  caucvgb  15582  fsumrlim  15713  fsumo1  15714  ntrivcvg  15799  rplpwr  16464  dvdssq  16473  nn0seqcvgd  16476  lcmgcdlem  16512  isprm6  16620  phiprmpw  16682  pcneg  16781  prmpwdvds  16811  4sqlem19  16870  0ramcl  16930  imasleval  17440  catpropd  17610  funcres2c  17805  initoeu2  17918  oduprs  18201  latdisdlem  18397  acsfiindd  18454  dirtr  18503  chnind  18522  mndpsuppss  18668  mndind  18731  grpinveu  18882  mulgnn0subcl  18995  mulgsubcl  18996  mhmmulg  19023  cycsubm  19109  cycsubgcl  19113  cycsubgss  19114  ghmmulg  19135  odf1  19469  dfod2  19471  gexdvds2  19492  sylow2blem3  19529  frgpup1  19682  iscyggen2  19788  iscyg3  19793  prdsgsum  19888  ringrghm  20226  dvdsrcl2  20279  crngunit  20291  dvdsrpropd  20329  lss1d  20891  quscrng  21215  mulgghm2  21408  frgpcyg  21505  ip0r  21569  isphld  21586  frlmgsum  21704  uvcresum  21725  psdmul  22076  coe1tmmul  22186  mdetdiagid  22510  cpmatmcllem  22628  tgcl  22879  0ntr  22981  innei  23035  neitr  23090  ordtrest2lem  23113  cncnp  23190  cnnei  23192  2ndcdisj  23366  dislly  23407  dissnlocfin  23439  kgenss  23453  ptcnplem  23531  ptcnp  23532  ptcn  23537  cnmpt2k  23598  qtoprest  23627  kqt0lem  23646  isr0  23647  kqreglem1  23651  trfilss  23799  isufil2  23818  ufileu  23829  hausflim  23891  cnextcn  23977  symgtgp  24016  tsmssubm  24053  tsmsxplem1  24063  ustfilxp  24123  ustuqtop0  24150  elbl2ps  24299  elbl2  24300  nrginvrcn  24602  nmoix  24639  nmoleub  24641  cncfco  24822  icccvx  24870  iscmet3  25215  rrxmet  25330  ovolfioo  25390  ovolficc  25391  ovolicc2lem4  25443  iunmbl2  25480  dyadmax  25521  mbfsup  25587  mbflimsup  25589  mbflim  25591  itg1addlem4  25622  mbfi1flimlem  25645  itg2monolem1  25673  itg2mono  25676  itg2i1fseqle  25677  itg2i1fseq  25678  itg2addlem  25681  itg2gt0  25683  itg2cnlem1  25684  itgfsum  25750  cnlimc  25811  dvlip2  25922  itgsubst  25978  plyeq0lem  26137  plypf1  26139  dvtaylp  26300  ulmcaulem  26325  ulmcau  26326  ulmcn  26330  ulmdvlem3  26333  mtest  26335  pserulm  26353  pserdvlem2  26360  logdivlt  26552  advlogexp  26586  cxpexp  26599  cxpcl  26605  xrlimcnp  26900  basellem4  27016  logexprlim  27158  dchrsum2  27201  sumdchr2  27203  rpvmasum2  27445  pntrsumbnd2  27500  pntleml  27544  noreson  27594  zs12zodd  28387  tglineeltr  28604  brbtwn2  28878  colinearalglem4  28882  axeuclidlem  28935  axcontlem8  28944  axcontlem10  28946  grpoidinvlem3  30478  grpoideu  30481  grpoinveu  30491  nmcvcn  30667  nmounbi  30748  blocnilem  30776  ubthlem1  30842  h2hlm  30952  ocsh  31255  brafnmul  31923  kbpj  31928  nmcexi  31998  lnconi  32005  riesz1  32037  mdbr2  32268  mdsl0  32282  mdslmd3i  32304  csmdsymi  32306  atcvatlem  32357  chirredlem1  32362  chirredi  32366  cdj3lem2b  32409  xrge0infss  32735  mgcmntco  32967  lmodvslmhm  33022  gsumwrd2dccatlem  33038  submarchi  33147  dvdsruasso  33342  grplsm0l  33360  ssdifidllem  33413  ssdifidlprm  33415  ssmxidllem  33430  rprmndvdsru  33486  r1plmhm  33562  mplvrpmmhm  33568  mplvrpmrhm  33569  lindsunlem  33629  lindsun  33630  fldextrspunlsplem  33678  extdgfialglem2  33698  madjusmdetlem2  33833  zarcmplem  33886  ordtrest2NEWlem  33927  voliune  34234  fsum2dsub  34612  circlemeth  34645  bnj110  34862  cvxsconn  35279  btwnouttr2  36056  cgrxfr  36089  btwnxfr  36090  lineext  36110  segcon2  36139  brsegle2  36143  seglecgr12im  36144  segletr  36148  broutsideof3  36160  outsideofeu  36165  lineunray  36181  lineelsb2  36182  neibastop3  36396  bj-imdiridlem  37219  isbasisrelowllem1  37389  isbasisrelowllem2  37390  fvineqsneu  37445  unccur  37643  fin2solem  37646  lindsadd  37653  matunitlindflem1  37656  matunitlindflem2  37657  poimirlem4  37664  poimirlem6  37666  poimirlem7  37667  poimirlem22  37682  poimirlem23  37683  poimirlem25  37685  poimirlem26  37686  poimirlem28  37688  poimirlem30  37690  poimirlem31  37691  poimirlem32  37692  poimir  37693  broucube  37694  heicant  37695  mblfinlem3  37699  volsupnfl  37705  itg2addnclem  37711  itg2addnclem2  37712  itg2addnclem3  37713  ftc1anclem1  37733  ftc1anclem5  37737  ftc1anclem6  37738  ftc1anc  37741  unirep  37754  filbcmb  37780  fzmul  37781  fdc  37785  nninfnub  37791  isbnd2  37823  bndss  37826  prdsbnd  37833  prdstotbnd  37834  ismtyres  37848  rrnmet  37869  rrncmslem  37872  rrnequiv  37875  ghomco  37931  grpokerinj  37933  rngonegmn1l  37981  isdrngo2  37998  rngoisocnv  38021  divrngidl  38068  intidl  38069  unichnidl  38071  prnc  38107  isfldidl  38108  cvrexchlem  39458  ps-2  39517  3atnelvolN  39625  dib1dim  41204  dib1dim2  41207  f1o2d2  42266  expeqidd  42358  pwsgprod  42577  evlselv  42620  fsuppind  42623  mzpindd  42779  dvdsabsmod0  43020  radcnvrat  44347  expgrowth  44368  modelac8prim  45025  fnchoice  45066  infxrbnd2  45407  infleinflem2  45409  xrralrecnnge  45428  limsuppnfdlem  45739  icccncfext  45925  dvnmul  45981  dvnprodlem2  45985  stoweidlem17  46055  stoweidlem30  46068  stoweidlem38  46076  stoweidlem42  46080  stoweidlem44  46082  fourierdlem31  46176  fourierdlem73  46217  fourierdlem74  46218  fourierdlem75  46219  fourierdlem83  46227  fourierdlem94  46238  fourierdlem113  46257  etransclem4  46276  iinhoiicclem  46711  iccvonmbllem  46716  smfsuplem1  46849  smfsupdmmbllem  46882  smfinfdmmbllem  46886  itsclquadeu  48809  aacllem  49833