Theorem an32s 665

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 659	. 2 ⊢ (((𝜑 ∧ 𝜒) ∧ 𝜓) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒))
2		an32s.1	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
3	1, 2	sylbi 220	1 ⊢ (((𝜑 ∧ 𝜒) ∧ 𝜓) → 𝜃)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  anass1rs  668  anabss1  679  biadanid  835  wereu2  5660  ordintdif  6416  ordunisssuc  6473  fssres  6748  dffv2  6980  isocnv  7334  f1oiso  7355  f1ocnvfv3  7411  fiunlem  7941  mpof1o2d  8123  onfununi  8330  oev2  8510  oaordi  8533  oaass  8548  omlimcl  8565  odi  8566  omass  8567  oewordri  8580  oelim2  8583  oeoa  8585  oeoe  8587  nnaordi  8606  omabs  8639  eceqoveq  8822  mapxpen  9134  mapdom2  9139  findcard  9151  dif1ennnALT  9240  fimax2g  9249  isfinite2  9261  fimin2g  9462  rankval3b  9801  isf32lem9  10356  fin1a2s  10409  zornn0g  10500  gchen1  10621  gchen2  10622  intwun  10731  suplem2pr  11049  recexsrlem  11099  axpre-sup  11165  axsup  11296  dedekind  11384  recextlem2  11856  divne0  11895  dfinfre  12207  qreccl  13005  xrlttr  13177  xaddf  13262  xrsupsslem  13345  xrinfmsslem  13346  supxr2  13352  supxrunb1  13357  supxrbnd1  13359  supxrbnd2  13360  modid  13943  seqof  14109  cau3lem  15426  lo1bdd2  15595  o1co  15657  rlimcn3  15661  climcn1  15663  climcn2  15664  rlimsqzlem  15720  caucvgb  15751  fsumrlim  15882  fsumo1  15883  ntrivcvg  15970  rplpwr  16634  dvdssq  16643  nn0seqcvgd  16646  lcmgcdlem  16682  isprm6  16791  phiprmpw  16853  pcneg  16952  prmpwdvds  16982  4sqlem19  17041  0ramcl  17101  imasleval  17613  catpropd  17783  funcres2c  17978  initoeu2  18091  oduprs  18374  latdisdlem  18570  acsfiindd  18627  dirtr  18676  chnind  18695  mndpsuppss  18847  mndind  18911  grpinveu  19065  mulgnn0subcl  19177  mulgsubcl  19178  mhmmulg  19205  cycsubm  19297  cycsubgcl  19301  cycsubgss  19302  ghmmulg  19322  odf1  19656  dfod2  19658  gexdvds2  19679  sylow2blem3  19716  frgpup1  19869  iscyggen2  19975  iscyg3  19980  prdsgsum  20075  ringrghm  20422  pwsgprod  20437  dvdsrcl2  20474  crngunit  20486  dvdsrpropd  20524  isdrng3lem2  20882  lss1d  21114  quscrng  21453  ssdifidllem  21514  ssdifidlprm  21516  mulgghm2  21656  frgpcyg  21753  ip0r  21817  isphld  21834  frlmgsum  21952  uvcresum  21973  psdmul  22359  coe1tmmul  22468  mdetdiagid  22787  cpmatmcllem  22905  tgcl  23156  0ntr  23258  innei  23312  neitr  23367  ordtrest2lem  23390  cncnp  23467  cnnei  23469  2ndcdisj  23644  dislly  23685  dissnlocfin  23717  kgenss  23731  ptcnplem  23809  ptcnp  23810  ptcn  23815  cnmpt2k  23876  qtoprest  23905  kqt0lem  23924  isr0  23925  kqreglem1  23929  trfilss  24077  isufil2  24096  ufileu  24107  hausflim  24169  cnextcn  24255  symgtgp  24294  tsmssubm  24331  tsmsxplem1  24341  ustfilxp  24401  ustuqtop0  24428  elbl2ps  24577  elbl2  24578  nrginvrcn  24880  nmoix  24917  nmoleub  24919  cncfco  25097  icccvx  25140  iscmet3  25483  rrxmet  25598  ovolfioo  25657  ovolficc  25658  ovolicc2lem4  25710  iunmbl2  25747  dyadmax  25788  mbfsup  25854  mbflimsup  25856  mbflim  25858  itg1addlem4  25889  mbfi1flimlem  25912  itg2monolem1  25940  itg2mono  25943  itg2i1fseqle  25944  itg2i1fseq  25945  itg2addlem  25948  itg2gt0  25950  itg2cnlem1  25951  itgfsum  26017  cnlimc  26078  dvlip2  26185  itgsubst  26239  plyeq0lem  26398  plypf1  26400  dvtaylp  26564  ulmcaulem  26588  ulmcau  26589  ulmcn  26593  ulmdvlem3  26596  mtest  26598  pserulm  26616  pserdvlem2  26622  logdivlt  26817  advlogexp  26851  cxpexp  26864  cxpcl  26870  xrlimcnp  27164  basellem4  27279  logexprlim  27420  dchrsum2  27463  sumdchr2  27465  rpvmasum2  27707  pntrsumbnd2  27762  pntleml  27806  noreson  27855  z12zsodd  28706  tglineeltr  28935  plngrotlem2  29101  brbtwn2  29286  colinearalglem4  29290  axeuclidlem  29343  axcontlem8  29352  axcontlem10  29354  grpoidinvlem3  30905  grpoideu  30908  grpoinveu  30918  nmcvcn  31094  nmounbi  31175  blocnilem  31203  ubthlem1  31269  h2hlm  31379  ocsh  31682  brafnmul  32350  kbpj  32355  nmcexi  32425  lnconi  32432  riesz1  32464  mdbr2  32695  mdsl0  32709  mdslmd3i  32731  csmdsymi  32733  atcvatlem  32784  chirredlem1  32789  chirredi  32793  cdj3lem2b  32836  xrge0infss  33151  mgcmntco  33354  lmodvslmhm  33410  suppgsumssiun  33432  gsumwrd2dccatlem  33437  submarchi  33546  dvdsruasso  33738  grplsm0l  33752  ssmxidllem  33796  rprmndvdsru  33859  r1plmhm  33939  mplvrpmmhm  33976  mplvrpmrhm  33977  esplyfval1  34003  lindsunlem  34054  lindsun  34055  fldextrspunlsplem  34103  extdgfialglem2  34123  madjusmdetlem2  34258  zarcmplem  34311  ordtrest2NEWlem  34352  voliune  34660  fsum2dsub  35035  circlemeth  35068  bnj110  35287  cvxsconn  35748  btwnouttr2  36527  cgrxfr  36560  btwnxfr  36561  lineext  36581  segcon2  36610  brsegle2  36614  seglecgr12im  36615  segletr  36619  broutsideof3  36631  outsideofeu  36636  lineunray  36652  lineelsb2  36653  nmulrid  36702  neibastop3  36906  ttcmin  37040  mh-inf3f1  37085  bj-imdiridlem  37862  isbasisrelowllem1  38034  isbasisrelowllem2  38035  fvineqsneu  38090  unccur  38287  fin2solem  38290  lindsadd  38297  matunitlindflem1  38300  matunitlindflem2  38301  poimirlem4  38308  poimirlem6  38310  poimirlem7  38311  poimirlem22  38326  poimirlem23  38327  poimirlem25  38329  poimirlem26  38330  poimirlem28  38332  poimirlem30  38334  poimirlem31  38335  poimirlem32  38336  poimir  38337  broucube  38338  heicant  38339  mblfinlem3  38343  volsupnfl  38349  itg2addnclem  38355  itg2addnclem2  38356  itg2addnclem3  38357  ftc1anclem1  38377  ftc1anclem5  38381  ftc1anclem6  38382  ftc1anc  38385  unirep  38398  filbcmb  38424  fzmul  38425  fdc  38429  nninfnub  38435  isbnd2  38467  bndss  38470  prdsbnd  38477  prdstotbnd  38478  ismtyres  38492  rrnmet  38513  rrncmslem  38516  rrnequiv  38519  ghomco  38575  grpokerinj  38577  rngonegmn1l  38625  isdrngo2  38642  rngoisocnv  38665  divrngidl  38712  intidl  38713  unichnidl  38715  prnc  38751  isfldidl  38752  cvrexchlem  40226  ps-2  40285  3atnelvolN  40393  dib1dim  41972  dib1dim2  41975  expeqidd  43119  evlselv  43354  fsuppind  43355  mzpindd  43510  dvdsabsmod0  43747  radcnvrat  45057  expgrowth  45078  modelac8prim  45734  fnchoice  45782  infxrbnd2  46117  infleinflem2  46119  xrralrecnnge  46138  limsuppnfdlem  46448  icccncfext  46634  dvnmul  46690  dvnprodlem2  46694  stoweidlem17  46764  stoweidlem30  46777  stoweidlem38  46785  stoweidlem42  46789  stoweidlem44  46791  fourierdlem31  46885  fourierdlem73  46926  fourierdlem74  46927  fourierdlem75  46928  fourierdlem83  46936  fourierdlem94  46947  fourierdlem113  46966  etransclem4  46985  hoicvr  47295  iinhoiicclem  47420  iccvonmbllem  47425  smfsuplem1  47558  smfsupdmmbllem  47591  smfinfdmmbllem  47595  itsclquadeu  49590  aacllem  50654