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  5621  ordintdif  6368  ordunisssuc  6425  fssres  6700  dffv2  6929  isocnv  7276  f1oiso  7297  f1ocnvfv3  7353  fiunlem  7886  onfununi  8273  oev2  8450  oaordi  8473  oaass  8488  omlimcl  8505  odi  8506  omass  8507  oewordri  8520  oelim2  8523  oeoa  8525  oeoe  8527  nnaordi  8546  omabs  8579  eceqoveq  8759  mapxpen  9071  mapdom2  9076  findcard  9088  dif1ennnALT  9177  fimax2g  9186  isfinite2  9198  fimin2g  9402  rankval3b  9738  isf32lem9  10271  fin1a2s  10324  zornn0g  10415  gchen1  10536  gchen2  10537  intwun  10646  suplem2pr  10964  recexsrlem  11014  axpre-sup  11080  axsup  11208  dedekind  11296  recextlem2  11768  divne0  11808  dfinfre  12123  qreccl  12882  xrlttr  13054  xaddf  13139  xrsupsslem  13222  xrinfmsslem  13223  supxr2  13229  supxrunb1  13234  supxrbnd1  13236  supxrbnd2  13237  modid  13816  seqof  13982  cau3lem  15278  lo1bdd2  15447  o1co  15509  rlimcn3  15513  climcn1  15515  climcn2  15516  rlimsqzlem  15572  caucvgb  15603  fsumrlim  15734  fsumo1  15735  ntrivcvg  15820  rplpwr  16485  dvdssq  16494  nn0seqcvgd  16497  lcmgcdlem  16533  isprm6  16641  phiprmpw  16703  pcneg  16802  prmpwdvds  16832  4sqlem19  16891  0ramcl  16951  imasleval  17462  catpropd  17632  funcres2c  17827  initoeu2  17940  oduprs  18223  latdisdlem  18419  acsfiindd  18476  dirtr  18525  chnind  18544  mndpsuppss  18690  mndind  18753  grpinveu  18904  mulgnn0subcl  19017  mulgsubcl  19018  mhmmulg  19045  cycsubm  19131  cycsubgcl  19135  cycsubgss  19136  ghmmulg  19157  odf1  19491  dfod2  19493  gexdvds2  19514  sylow2blem3  19551  frgpup1  19704  iscyggen2  19810  iscyg3  19815  prdsgsum  19910  ringrghm  20248  pwsgprod  20265  dvdsrcl2  20302  crngunit  20314  dvdsrpropd  20352  lss1d  20914  quscrng  21238  mulgghm2  21431  frgpcyg  21528  ip0r  21592  isphld  21609  frlmgsum  21727  uvcresum  21748  psdmul  22109  coe1tmmul  22219  mdetdiagid  22544  cpmatmcllem  22662  tgcl  22913  0ntr  23015  innei  23069  neitr  23124  ordtrest2lem  23147  cncnp  23224  cnnei  23226  2ndcdisj  23400  dislly  23441  dissnlocfin  23473  kgenss  23487  ptcnplem  23565  ptcnp  23566  ptcn  23571  cnmpt2k  23632  qtoprest  23661  kqt0lem  23680  isr0  23681  kqreglem1  23685  trfilss  23833  isufil2  23852  ufileu  23863  hausflim  23925  cnextcn  24011  symgtgp  24050  tsmssubm  24087  tsmsxplem1  24097  ustfilxp  24157  ustuqtop0  24184  elbl2ps  24333  elbl2  24334  nrginvrcn  24636  nmoix  24673  nmoleub  24675  cncfco  24856  icccvx  24904  iscmet3  25249  rrxmet  25364  ovolfioo  25424  ovolficc  25425  ovolicc2lem4  25477  iunmbl2  25514  dyadmax  25555  mbfsup  25621  mbflimsup  25623  mbflim  25625  itg1addlem4  25656  mbfi1flimlem  25679  itg2monolem1  25707  itg2mono  25710  itg2i1fseqle  25711  itg2i1fseq  25712  itg2addlem  25715  itg2gt0  25717  itg2cnlem1  25718  itgfsum  25784  cnlimc  25845  dvlip2  25956  itgsubst  26012  plyeq0lem  26171  plypf1  26173  dvtaylp  26334  ulmcaulem  26359  ulmcau  26360  ulmcn  26364  ulmdvlem3  26367  mtest  26369  pserulm  26387  pserdvlem2  26394  logdivlt  26586  advlogexp  26620  cxpexp  26633  cxpcl  26639  xrlimcnp  26934  basellem4  27050  logexprlim  27192  dchrsum2  27235  sumdchr2  27237  rpvmasum2  27479  pntrsumbnd2  27534  pntleml  27578  noreson  27628  z12zsodd  28478  tglineeltr  28703  brbtwn2  28978  colinearalglem4  28982  axeuclidlem  29035  axcontlem8  29044  axcontlem10  29046  grpoidinvlem3  30581  grpoideu  30584  grpoinveu  30594  nmcvcn  30770  nmounbi  30851  blocnilem  30879  ubthlem1  30945  h2hlm  31055  ocsh  31358  brafnmul  32026  kbpj  32031  nmcexi  32101  lnconi  32108  riesz1  32140  mdbr2  32371  mdsl0  32385  mdslmd3i  32407  csmdsymi  32409  atcvatlem  32460  chirredlem1  32465  chirredi  32469  cdj3lem2b  32512  xrge0infss  32840  mgcmntco  33076  lmodvslmhm  33133  gsumwrd2dccatlem  33159  submarchi  33268  dvdsruasso  33466  grplsm0l  33484  ssdifidllem  33537  ssdifidlprm  33539  ssmxidllem  33554  rprmndvdsru  33610  r1plmhm  33691  mplvrpmmhm  33711  mplvrpmrhm  33712  lindsunlem  33781  lindsun  33782  fldextrspunlsplem  33830  extdgfialglem2  33850  madjusmdetlem2  33985  zarcmplem  34038  ordtrest2NEWlem  34079  voliune  34386  fsum2dsub  34764  circlemeth  34797  bnj110  35014  cvxsconn  35437  btwnouttr2  36216  cgrxfr  36249  btwnxfr  36250  lineext  36270  segcon2  36299  brsegle2  36303  seglecgr12im  36304  segletr  36308  broutsideof3  36320  outsideofeu  36325  lineunray  36341  lineelsb2  36342  neibastop3  36556  bj-imdiridlem  37390  isbasisrelowllem1  37560  isbasisrelowllem2  37561  fvineqsneu  37616  unccur  37804  fin2solem  37807  lindsadd  37814  matunitlindflem1  37817  matunitlindflem2  37818  poimirlem4  37825  poimirlem6  37827  poimirlem7  37828  poimirlem22  37843  poimirlem23  37844  poimirlem25  37846  poimirlem26  37847  poimirlem28  37849  poimirlem30  37851  poimirlem31  37852  poimirlem32  37853  poimir  37854  broucube  37855  heicant  37856  mblfinlem3  37860  volsupnfl  37866  itg2addnclem  37872  itg2addnclem2  37873  itg2addnclem3  37874  ftc1anclem1  37894  ftc1anclem5  37898  ftc1anclem6  37899  ftc1anc  37902  unirep  37915  filbcmb  37941  fzmul  37942  fdc  37946  nninfnub  37952  isbnd2  37984  bndss  37987  prdsbnd  37994  prdstotbnd  37995  ismtyres  38009  rrnmet  38030  rrncmslem  38033  rrnequiv  38036  ghomco  38092  grpokerinj  38094  rngonegmn1l  38142  isdrngo2  38159  rngoisocnv  38182  divrngidl  38229  intidl  38230  unichnidl  38232  prnc  38268  isfldidl  38269  cvrexchlem  39679  ps-2  39738  3atnelvolN  39846  dib1dim  41425  dib1dim2  41428  f1o2d2  42489  expeqidd  42580  evlselv  42830  fsuppind  42833  mzpindd  42988  dvdsabsmod0  43229  radcnvrat  44555  expgrowth  44576  modelac8prim  45233  fnchoice  45274  infxrbnd2  45613  infleinflem2  45615  xrralrecnnge  45634  limsuppnfdlem  45945  icccncfext  46131  dvnmul  46187  dvnprodlem2  46191  stoweidlem17  46261  stoweidlem30  46274  stoweidlem38  46282  stoweidlem42  46286  stoweidlem44  46288  fourierdlem31  46382  fourierdlem73  46423  fourierdlem74  46424  fourierdlem75  46425  fourierdlem83  46433  fourierdlem94  46444  fourierdlem113  46463  etransclem4  46482  iinhoiicclem  46917  iccvonmbllem  46922  smfsuplem1  47055  smfsupdmmbllem  47088  smfinfdmmbllem  47092  itsclquadeu  49023  aacllem  50046