Theorem an32s 653

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 647	. 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  656  anabss1  667  biadanid  823  wereu2  5621  ordintdif  6368  ordunisssuc  6425  fssres  6700  dffv2  6929  isocnv  7278  f1oiso  7299  f1ocnvfv3  7355  fiunlem  7888  onfununi  8274  oev2  8451  oaordi  8474  oaass  8489  omlimcl  8506  odi  8507  omass  8508  oewordri  8521  oelim2  8524  oeoa  8526  oeoe  8528  nnaordi  8547  omabs  8580  eceqoveq  8762  mapxpen  9074  mapdom2  9079  findcard  9091  dif1ennnALT  9180  fimax2g  9189  isfinite2  9201  fimin2g  9405  rankval3b  9741  isf32lem9  10274  fin1a2s  10327  zornn0g  10418  gchen1  10539  gchen2  10540  intwun  10649  suplem2pr  10967  recexsrlem  11017  axpre-sup  11083  axsup  11212  dedekind  11300  recextlem2  11772  divne0  11812  dfinfre  12128  qreccl  12910  xrlttr  13082  xaddf  13167  xrsupsslem  13250  xrinfmsslem  13251  supxr2  13257  supxrunb1  13262  supxrbnd1  13264  supxrbnd2  13265  modid  13846  seqof  14012  cau3lem  15308  lo1bdd2  15477  o1co  15539  rlimcn3  15543  climcn1  15545  climcn2  15546  rlimsqzlem  15602  caucvgb  15633  fsumrlim  15765  fsumo1  15766  ntrivcvg  15853  rplpwr  16518  dvdssq  16527  nn0seqcvgd  16530  lcmgcdlem  16566  isprm6  16675  phiprmpw  16737  pcneg  16836  prmpwdvds  16866  4sqlem19  16925  0ramcl  16985  imasleval  17496  catpropd  17666  funcres2c  17861  initoeu2  17974  oduprs  18257  latdisdlem  18453  acsfiindd  18510  dirtr  18559  chnind  18578  mndpsuppss  18724  mndind  18787  grpinveu  18941  mulgnn0subcl  19054  mulgsubcl  19055  mhmmulg  19082  cycsubm  19168  cycsubgcl  19172  cycsubgss  19173  ghmmulg  19194  odf1  19528  dfod2  19530  gexdvds2  19551  sylow2blem3  19588  frgpup1  19741  iscyggen2  19847  iscyg3  19852  prdsgsum  19947  ringrghm  20285  pwsgprod  20300  dvdsrcl2  20337  crngunit  20349  dvdsrpropd  20387  lss1d  20949  quscrng  21273  mulgghm2  21466  frgpcyg  21563  ip0r  21627  isphld  21644  frlmgsum  21762  uvcresum  21783  psdmul  22142  coe1tmmul  22252  mdetdiagid  22575  cpmatmcllem  22693  tgcl  22944  0ntr  23046  innei  23100  neitr  23155  ordtrest2lem  23178  cncnp  23255  cnnei  23257  2ndcdisj  23431  dislly  23472  dissnlocfin  23504  kgenss  23518  ptcnplem  23596  ptcnp  23597  ptcn  23602  cnmpt2k  23663  qtoprest  23692  kqt0lem  23711  isr0  23712  kqreglem1  23716  trfilss  23864  isufil2  23883  ufileu  23894  hausflim  23956  cnextcn  24042  symgtgp  24081  tsmssubm  24118  tsmsxplem1  24128  ustfilxp  24188  ustuqtop0  24215  elbl2ps  24364  elbl2  24365  nrginvrcn  24667  nmoix  24704  nmoleub  24706  cncfco  24884  icccvx  24927  iscmet3  25270  rrxmet  25385  ovolfioo  25444  ovolficc  25445  ovolicc2lem4  25497  iunmbl2  25534  dyadmax  25575  mbfsup  25641  mbflimsup  25643  mbflim  25645  itg1addlem4  25676  mbfi1flimlem  25699  itg2monolem1  25727  itg2mono  25730  itg2i1fseqle  25731  itg2i1fseq  25732  itg2addlem  25735  itg2gt0  25737  itg2cnlem1  25738  itgfsum  25804  cnlimc  25865  dvlip2  25972  itgsubst  26026  plyeq0lem  26185  plypf1  26187  dvtaylp  26347  ulmcaulem  26372  ulmcau  26373  ulmcn  26377  ulmdvlem3  26380  mtest  26382  pserulm  26400  pserdvlem2  26406  logdivlt  26598  advlogexp  26632  cxpexp  26645  cxpcl  26651  xrlimcnp  26945  basellem4  27061  logexprlim  27202  dchrsum2  27245  sumdchr2  27247  rpvmasum2  27489  pntrsumbnd2  27544  pntleml  27588  noreson  27638  z12zsodd  28488  tglineeltr  28713  brbtwn2  28988  colinearalglem4  28992  axeuclidlem  29045  axcontlem8  29054  axcontlem10  29056  grpoidinvlem3  30592  grpoideu  30595  grpoinveu  30605  nmcvcn  30781  nmounbi  30862  blocnilem  30890  ubthlem1  30956  h2hlm  31066  ocsh  31369  brafnmul  32037  kbpj  32042  nmcexi  32112  lnconi  32119  riesz1  32151  mdbr2  32382  mdsl0  32396  mdslmd3i  32418  csmdsymi  32420  atcvatlem  32471  chirredlem1  32476  chirredi  32480  cdj3lem2b  32523  xrge0infss  32848  mgcmntco  33069  lmodvslmhm  33126  suppgsumssiun  33148  gsumwrd2dccatlem  33153  submarchi  33262  dvdsruasso  33460  grplsm0l  33478  ssdifidllem  33531  ssdifidlprm  33533  ssmxidllem  33548  rprmndvdsru  33604  r1plmhm  33685  mplvrpmmhm  33705  mplvrpmrhm  33706  esplyfval1  33732  lindsunlem  33784  lindsun  33785  fldextrspunlsplem  33833  extdgfialglem2  33853  madjusmdetlem2  33988  zarcmplem  34041  ordtrest2NEWlem  34082  voliune  34389  fsum2dsub  34767  circlemeth  34800  bnj110  35016  cvxsconn  35441  btwnouttr2  36220  cgrxfr  36253  btwnxfr  36254  lineext  36274  segcon2  36303  brsegle2  36307  seglecgr12im  36308  segletr  36312  broutsideof3  36324  outsideofeu  36329  lineunray  36345  lineelsb2  36346  neibastop3  36560  ttcmin  36694  mh-inf3f1  36739  bj-imdiridlem  37515  isbasisrelowllem1  37685  isbasisrelowllem2  37686  fvineqsneu  37741  unccur  37938  fin2solem  37941  lindsadd  37948  matunitlindflem1  37951  matunitlindflem2  37952  poimirlem4  37959  poimirlem6  37961  poimirlem7  37962  poimirlem22  37977  poimirlem23  37978  poimirlem25  37980  poimirlem26  37981  poimirlem28  37983  poimirlem30  37985  poimirlem31  37986  poimirlem32  37987  poimir  37988  broucube  37989  heicant  37990  mblfinlem3  37994  volsupnfl  38000  itg2addnclem  38006  itg2addnclem2  38007  itg2addnclem3  38008  ftc1anclem1  38028  ftc1anclem5  38032  ftc1anclem6  38033  ftc1anc  38036  unirep  38049  filbcmb  38075  fzmul  38076  fdc  38080  nninfnub  38086  isbnd2  38118  bndss  38121  prdsbnd  38128  prdstotbnd  38129  ismtyres  38143  rrnmet  38164  rrncmslem  38167  rrnequiv  38170  ghomco  38226  grpokerinj  38228  rngonegmn1l  38276  isdrngo2  38293  rngoisocnv  38316  divrngidl  38363  intidl  38364  unichnidl  38366  prnc  38402  isfldidl  38403  cvrexchlem  39879  ps-2  39938  3atnelvolN  40046  dib1dim  41625  dib1dim2  41628  f1o2d2  42688  expeqidd  42771  evlselv  43034  fsuppind  43037  mzpindd  43192  dvdsabsmod0  43433  radcnvrat  44759  expgrowth  44780  modelac8prim  45437  fnchoice  45478  infxrbnd2  45816  infleinflem2  45818  xrralrecnnge  45837  limsuppnfdlem  46147  icccncfext  46333  dvnmul  46389  dvnprodlem2  46393  stoweidlem17  46463  stoweidlem30  46476  stoweidlem38  46484  stoweidlem42  46488  stoweidlem44  46490  fourierdlem31  46584  fourierdlem73  46625  fourierdlem74  46626  fourierdlem75  46627  fourierdlem83  46635  fourierdlem94  46646  fourierdlem113  46665  etransclem4  46684  hoicvr  46994  iinhoiicclem  47119  iccvonmbllem  47124  smfsuplem1  47257  smfsupdmmbllem  47290  smfinfdmmbllem  47294  itsclquadeu  49265  aacllem  50288