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  5647  ordintdif  6416  ordunisssuc  6473  fssres  6751  dffv2  6983  isocnv  7340  f1oiso  7361  f1ocnvfv3  7417  fiunlem  7956  mpof1o2d  8141  onfununi  8354  oev2  8536  oaordi  8559  oaass  8574  omlimcl  8591  odi  8592  omass  8593  oewordri  8606  oelim2  8609  oeoa  8611  oeoe  8613  nnaordi  8632  omabs  8665  eceqoveq  8848  mapxpen  9167  mapdom2  9172  findcard  9184  dif1ennnALT  9273  fimax2g  9282  isfinite2  9295  fimin2g  9496  rankval3b  9841  isf32lem9  10444  fin1a2s  10497  zornn0g  10588  gchen1  10715  gchen2  10716  intwun  10825  suplem2pr  11143  recexsrlem  11193  axpre-sup  11259  axsup  11390  dedekind  11478  recextlem2  11952  divne0  11991  dfinfre  12303  qreccl  13102  xrlttr  13274  xaddf  13359  xrsupsslem  13442  xrinfmsslem  13443  supxr2  13449  supxrunb1  13454  supxrbnd1  13456  supxrbnd2  13457  modid  14041  seqof  14207  cau3lem  15529  lo1bdd2  15698  o1co  15760  rlimcn3  15764  climcn1  15766  climcn2  15767  rlimsqzlem  15823  caucvgb  15854  fsumrlim  15985  fsumo1  15986  ntrivcvg  16073  rplpwr  16739  dvdssq  16749  nn0seqcvgd  16752  lcmgcdlem  16788  isprm6  16897  phiprmpw  16960  pcneg  17059  prmpwdvds  17089  4sqlem19  17148  0ramcl  17208  imasleval  17720  catpropd  17890  funcres2c  18085  initoeu2  18198  oduprs  18481  latdisdlem  18677  acsfiindd  18734  dirtr  18783  chnind  18802  mndpsuppss  18966  mndind  19031  grpinveu  19192  mulgnn0subcl  19304  mulgsubcl  19305  mhmmulg  19332  cycsubm  19424  cycsubgcl  19428  cycsubgss  19429  ghmmulg  19449  odf1  19783  dfod2  19785  gexdvds2  19806  sylow2blem3  19843  frgpup1  19996  iscyggen2  20102  iscyg3  20107  prdsgsum  20202  ringrghm  20551  pwsgprod  20566  dvdsrcl2  20603  crngunit  20615  dvdsrpropd  20653  isdrng3lem2  21013  lss1d  21245  quscrng  21586  ssdifidllem  21647  ssdifidlprm  21649  mulgghm2  21789  frgpcyg  21886  ip0r  21950  isphld  21967  frlmgsum  22085  uvcresum  22106  psdmul  22494  coe1tmmul  22603  mdetdiagid  22922  matunitlindflem1  23001  matunitlindflem2  23002  cpmatmcllem  23043  tgcl  23294  0ntr  23396  innei  23450  neitr  23505  ordtrest2lem  23528  cncnp  23605  cnnei  23607  2ndcdisj  23782  dislly  23823  dissnlocfin  23855  kgenss  23869  ptcnplem  23947  ptcnp  23948  ptcn  23953  cnmpt2k  24014  qtoprest  24043  kqt0lem  24062  isr0  24063  kqreglem1  24067  trfilss  24215  isufil2  24234  ufileu  24245  hausflim  24307  cnextcn  24393  symgtgp  24432  tsmssubm  24469  tsmsxplem1  24479  ustfilxp  24539  ustuqtop0  24566  elbl2ps  24715  elbl2  24716  nrginvrcn  25018  nmoix  25055  nmoleub  25057  cncfco  25235  icccvx  25278  iscmet3  25621  rrxmet  25736  ovolfioo  25795  ovolficc  25796  ovolicc2lem4  25848  iunmbl2  25885  dyadmax  25926  mbfsup  25992  mbflimsup  25994  mbflim  25996  itg1addlem4  26027  mbfi1flimlem  26050  itg2monolem1  26078  itg2mono  26081  itg2i1fseqle  26082  itg2i1fseq  26083  itg2addlem  26086  itg2gt0  26088  itg2cnlem1  26089  itgfsum  26154  cnlimc  26215  dvlip2  26322  itgsubst  26376  plyeq0lem  26536  plypf1  26538  dvtaylp  26704  ulmcaulem  26728  ulmcau  26729  ulmcn  26733  ulmdvlem3  26736  mtest  26738  pserulm  26756  pserdvlem2  26762  logdivlt  26956  advlogexp  26990  cxpexp  27003  cxpcl  27009  xrlimcnp  27303  basellem4  27418  logexprlim  27559  dchrsum2  27602  sumdchr2  27604  rpvmasum2  27846  pntrsumbnd2  27901  pntleml  27945  noreson  28024  z12zsodd  28875  tglineeltr  29106  plngrotlem2  29273  brbtwn2  29490  colinearalglem4  29494  axeuclidlem  29547  axcontlem8  29556  axcontlem10  29558  grpoidinvlem3  31115  grpoideu  31118  grpoinveu  31128  nmcvcn  31304  nmounbi  31385  blocnilem  31413  ubthlem1  31479  h2hlm  31589  ocsh  31892  brafnmul  32560  kbpj  32565  nmcexi  32635  lnconi  32642  riesz1  32674  mdbr2  32905  mdsl0  32919  mdslmd3i  32941  csmdsymi  32943  atcvatlem  32994  chirredlem1  32999  chirredi  33003  cdj3lem2b  33046  xrge0infss  33400  mgcmntco  33603  lmodvslmhm  33659  suppgsumssiun  33681  gsumwrd2dccatlem  33686  submarchi  33795  dvdsruasso  33988  grplsm0l  34002  ssmxidllem  34046  rprmndvdsru  34109  r1plmhm  34189  mplvrpmmhm  34226  mplvrpmrhm  34227  esplyfval1  34253  lindsunlem  34304  lindsun  34305  fldextrspunlsplem  34353  extdgfialglem2  34373  madjusmdetlem2  34508  zarcmplem  34561  ordtrest2NEWlem  34602  voliune  34910  fsum2dsub  35284  circlemeth  35317  bnj110  35536  cvxsconn  36096  btwnouttr2  36881  cgrxfr  36914  btwnxfr  36915  lineext  36935  segcon2  36964  brsegle2  36968  seglecgr12im  36969  segletr  36973  broutsideof3  36985  outsideofeu  36990  lineunray  37006  lineelsb2  37007  nmulrid  37040  neibastop3  37244  ttcmin  37378  bj-imdiridlem  38213  isbasisrelowllem1  38385  isbasisrelowllem2  38386  fvineqsneu  38441  unccur  38633  fin2solem  38636  lindsadd  38643  poimirlem4  38649  poimirlem6  38651  poimirlem7  38652  poimirlem22  38667  poimirlem23  38668  poimirlem25  38670  poimirlem26  38671  poimirlem28  38673  poimirlem30  38675  poimirlem31  38676  poimirlem32  38677  poimir  38678  broucube  38679  heicant  38680  mblfinlem3  38684  volsupnfl  38690  itg2addnclem  38696  itg2addnclem2  38697  itg2addnclem3  38698  ftc1anclem1  38718  ftc1anclem5  38722  ftc1anclem6  38723  ftc1anc  38726  unirep  38755  filbcmb  38781  fzmul  38782  fdc  38786  nninfnub  38792  isbnd2  38824  bndss  38827  prdsbnd  38834  prdstotbnd  38835  ismtyres  38849  rrnmet  38870  rrncmslem  38873  rrnequiv  38876  ghomco  38932  grpokerinj  38934  rngonegmn1l  38982  isdrngo2  38999  rngoisocnv  39022  divrngidl  39069  intidl  39070  unichnidl  39072  prnc  39108  isfldidl  39109  cvrexchlem  40583  ps-2  40642  3atnelvolN  40750  dib1dim  42329  dib1dim2  42332  expeqidd  43489  evlselv  43724  fsuppind  43725  mzpindd  43864  dvdsabsmod0  44101  radcnvrat  45405  expgrowth  45426  modelac8prim  46089  fnchoice  46153  infxrbnd2  46487  infleinflem2  46489  xrralrecnnge  46508  limsuppnfdlem  46818  icccncfext  47004  dvnmul  47060  dvnprodlem2  47064  stoweidlem17  47134  stoweidlem30  47147  stoweidlem38  47155  stoweidlem42  47159  stoweidlem44  47161  fourierdlem31  47255  fourierdlem73  47296  fourierdlem74  47297  fourierdlem75  47298  fourierdlem83  47306  fourierdlem94  47317  fourierdlem113  47336  etransclem4  47355  hoicvr  47665  iinhoiicclem  47790  iccvonmbllem  47795  smfsuplem1  47928  smfsupdmmbllem  47961  smfinfdmmbllem  47965  itsclquadeu  49996  aacllem  51121  veroquadmodzerod  51166