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 220	1 ⊢ (((𝜑 ∧ 𝜒) ∧ 𝜓) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  anass1rs  655  anabss1  666  wereu2  5516  ordintdif  6215  ordunisssuc  6268  fssres  6538  foco  6598  dffv2  6757  isocnv  7090  f1oiso  7111  f1ocnvfv3  7160  fiunlem  7661  onfununi  8000  oev2  8172  oaordi  8196  oaass  8211  omlimcl  8228  odi  8229  omass  8230  oewordri  8242  oelim2  8245  oeoa  8247  oeoe  8249  nnaordi  8268  omabs  8298  eceqoveq  8426  mapxpen  8726  mapdom2  8731  findcard  8755  dif1enOLD  8821  fimax2g  8831  isfinite2  8843  fimin2g  9027  rankval3b  9321  isf32lem9  9854  fin1a2s  9907  zornn0g  9998  gchen1  10118  gchen2  10119  intwun  10228  suplem2pr  10546  recexsrlem  10596  axpre-sup  10662  axsup  10787  dedekind  10874  recextlem2  11342  divne0  11381  dfinfre  11692  qreccl  12444  xrlttr  12609  xaddf  12693  xrsupsslem  12776  xrinfmsslem  12777  supxr2  12783  supxrunb1  12788  supxrbnd1  12790  supxrbnd2  12791  modid  13348  seqof  13512  cau3lem  14797  lo1bdd2  14964  o1co  15026  rlimcn3  15030  climcn1  15032  climcn2  15033  rlimsqzlem  15091  caucvgb  15122  fsumrlim  15252  fsumo1  15253  ntrivcvg  15338  rplpwr  15996  dvdssq  16001  nn0seqcvgd  16004  lcmgcdlem  16040  isprm6  16148  phiprmpw  16206  pcneg  16303  prmpwdvds  16333  4sqlem19  16392  0ramcl  16452  imasleval  16910  catpropd  17076  funcres2c  17269  initoeu2  17381  acsfiindd  17896  latdisdlem  17908  dirtr  17955  mndind  18101  grpinveu  18249  mulgnn0subcl  18352  mulgsubcl  18353  mhmmulg  18379  cycsubm  18456  cycsubgcl  18460  cycsubgss  18461  ghmmulg  18481  odf1  18800  dfod2  18802  gexdvds2  18821  sylow2blem3  18858  frgpup1  19012  iscyggen2  19112  iscyg3  19117  prdsgsum  19213  ringrghm  19470  dvdsrcl2  19515  crngunit  19527  dvdsrpropd  19561  lss1d  19847  quscrng  20125  mulgghm2  20310  frgpcyg  20385  ip0r  20446  isphld  20463  frlmgsum  20581  uvcresum  20602  coe1tmmul  21045  mdetdiagid  21344  cpmatmcllem  21462  tgcl  21713  0ntr  21815  innei  21869  neitr  21924  ordtrest2lem  21947  cncnp  22024  cnnei  22026  2ndcdisj  22200  dislly  22241  dissnlocfin  22273  kgenss  22287  ptcnplem  22365  ptcnp  22366  ptcn  22371  cnmpt2k  22432  qtoprest  22461  kqt0lem  22480  isr0  22481  kqreglem1  22485  trfilss  22633  isufil2  22652  ufileu  22663  hausflim  22725  cnextcn  22811  symgtgp  22850  tsmssubm  22887  tsmsxplem1  22897  ustfilxp  22957  ustuqtop0  22985  elbl2ps  23135  elbl2  23136  nrginvrcn  23438  nmoix  23475  nmoleub  23477  cncfco  23652  icccvx  23695  iscmet3  24038  rrxmet  24153  ovolfioo  24212  ovolficc  24213  ovolicc2lem4  24265  iunmbl2  24302  dyadmax  24343  mbfsup  24409  mbflimsup  24411  mbflim  24413  itg1addlem4  24444  mbfi1flimlem  24467  itg2monolem1  24495  itg2mono  24498  itg2i1fseqle  24499  itg2i1fseq  24500  itg2addlem  24503  itg2gt0  24505  itg2cnlem1  24506  itgfsum  24571  cnlimc  24632  dvlip2  24739  itgsubst  24793  plyeq0lem  24951  plypf1  24953  dvtaylp  25109  ulmcaulem  25133  ulmcau  25134  ulmcn  25138  ulmdvlem3  25141  mtest  25143  pserulm  25161  pserdvlem2  25167  logdivlt  25356  advlogexp  25390  cxpexp  25403  cxpcl  25409  xrlimcnp  25698  basellem4  25813  logexprlim  25953  dchrsum2  25996  sumdchr2  25998  rpvmasum2  26240  pntrsumbnd2  26295  pntleml  26339  tglineeltr  26569  brbtwn2  26843  colinearalglem4  26847  axeuclidlem  26900  axcontlem8  26909  axcontlem10  26911  grpoidinvlem3  28433  grpoideu  28436  grpoinveu  28446  nmcvcn  28622  nmounbi  28703  blocnilem  28731  ubthlem1  28797  h2hlm  28907  ocsh  29210  brafnmul  29878  kbpj  29883  nmcexi  29953  lnconi  29960  riesz1  29992  mdbr2  30223  mdsl0  30237  mdslmd3i  30259  csmdsymi  30261  atcvatlem  30312  chirredlem1  30317  chirredi  30321  cdj3lem2b  30364  biadanid  30380  xrge0infss  30650  oduprs  30808  mgcmntco  30841  lmodvslmhm  30879  submarchi  31009  grplsm0l  31155  ssmxidllem  31205  lindsunlem  31269  lindsun  31270  madjusmdetlem2  31342  zarcmplem  31395  ordtrest2NEWlem  31436  voliune  31759  fsum2dsub  32149  circlemeth  32182  bnj110  32401  cvxsconn  32768  noreson  33496  btwnouttr2  33954  cgrxfr  33987  btwnxfr  33988  lineext  34008  segcon2  34037  brsegle2  34041  seglecgr12im  34042  segletr  34046  broutsideof3  34058  outsideofeu  34063  lineunray  34079  lineelsb2  34080  neibastop3  34181  bj-imdiridlem  34966  isbasisrelowllem1  35138  isbasisrelowllem2  35139  fvineqsneu  35194  unccur  35372  fin2solem  35375  lindsadd  35382  matunitlindflem1  35385  matunitlindflem2  35386  poimirlem4  35393  poimirlem6  35395  poimirlem7  35396  poimirlem22  35411  poimirlem23  35412  poimirlem25  35414  poimirlem26  35415  poimirlem28  35417  poimirlem30  35419  poimirlem31  35420  poimirlem32  35421  poimir  35422  broucube  35423  heicant  35424  mblfinlem3  35428  volsupnfl  35434  itg2addnclem  35440  itg2addnclem2  35441  itg2addnclem3  35442  ftc1anclem1  35462  ftc1anclem5  35466  ftc1anclem6  35467  ftc1anc  35470  unirep  35483  filbcmb  35510  fzmul  35511  fdc  35515  nninfnub  35521  isbnd2  35553  bndss  35556  prdsbnd  35563  prdstotbnd  35564  ismtyres  35578  rrnmet  35599  rrncmslem  35602  rrnequiv  35605  ghomco  35661  grpokerinj  35663  rngonegmn1l  35711  isdrngo2  35728  rngoisocnv  35751  divrngidl  35798  intidl  35799  unichnidl  35801  prnc  35837  isfldidl  35838  cvrexchlem  37045  ps-2  37104  3atnelvolN  37212  dib1dim  38791  dib1dim2  38794  pwsgprod  39834  fsuppind  39842  mzpindd  40124  dvdsabsmod0  40365  radcnvrat  41454  expgrowth  41475  fnchoice  42094  infxrbnd2  42430  infleinflem2  42432  xrralrecnnge  42452  limsuppnfdlem  42768  icccncfext  42954  dvnmul  43010  dvnprodlem2  43014  stoweidlem17  43084  stoweidlem30  43097  stoweidlem38  43105  stoweidlem42  43109  stoweidlem44  43111  fourierdlem31  43205  fourierdlem73  43246  fourierdlem74  43247  fourierdlem75  43248  fourierdlem83  43256  fourierdlem94  43267  fourierdlem113  43286  etransclem4  43305  iinhoiicclem  43737  iccvonmbllem  43742  smfsuplem1  43867  mndpsuppss  45225  itsclquadeu  45641  aacllem  45942