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  5648  ordintdif  6413  ordunisssuc  6470  fssres  6746  dffv2  6978  isocnv  7336  f1oiso  7357  f1ocnvfv3  7413  fiunlem  7952  mpof1o2d  8135  onfununi  8342  oev2  8524  oaordi  8547  oaass  8562  omlimcl  8579  odi  8580  omass  8581  oewordri  8594  oelim2  8597  oeoa  8599  oeoe  8601  nnaordi  8620  omabs  8653  eceqoveq  8836  mapxpen  9155  mapdom2  9160  findcard  9172  dif1ennnALT  9261  fimax2g  9270  isfinite2  9283  fimin2g  9484  rankval3b  9829  isf32lem9  10432  fin1a2s  10485  zornn0g  10576  gchen1  10703  gchen2  10704  intwun  10813  suplem2pr  11131  recexsrlem  11181  axpre-sup  11247  axsup  11378  dedekind  11466  recextlem2  11940  divne0  11979  dfinfre  12291  qreccl  13090  xrlttr  13262  xaddf  13347  xrsupsslem  13430  xrinfmsslem  13431  supxr2  13437  supxrunb1  13442  supxrbnd1  13444  supxrbnd2  13445  modid  14029  seqof  14195  cau3lem  15515  lo1bdd2  15684  o1co  15746  rlimcn3  15750  climcn1  15752  climcn2  15753  rlimsqzlem  15809  caucvgb  15840  fsumrlim  15971  fsumo1  15972  ntrivcvg  16059  rplpwr  16725  dvdssq  16735  nn0seqcvgd  16738  lcmgcdlem  16774  isprm6  16883  phiprmpw  16946  pcneg  17045  prmpwdvds  17075  4sqlem19  17134  0ramcl  17194  imasleval  17706  catpropd  17876  funcres2c  18071  initoeu2  18184  oduprs  18467  latdisdlem  18663  acsfiindd  18720  dirtr  18769  chnind  18788  mndpsuppss  18952  mndind  19017  grpinveu  19178  mulgnn0subcl  19290  mulgsubcl  19291  mhmmulg  19318  cycsubm  19410  cycsubgcl  19414  cycsubgss  19415  ghmmulg  19435  odf1  19769  dfod2  19771  gexdvds2  19792  sylow2blem3  19829  frgpup1  19982  iscyggen2  20088  iscyg3  20093  prdsgsum  20188  ringrghm  20537  pwsgprod  20552  dvdsrcl2  20589  crngunit  20601  dvdsrpropd  20639  isdrng3lem2  20999  lss1d  21231  quscrng  21572  ssdifidllem  21633  ssdifidlprm  21635  mulgghm2  21775  frgpcyg  21872  ip0r  21936  isphld  21953  frlmgsum  22071  uvcresum  22092  psdmul  22480  coe1tmmul  22589  mdetdiagid  22908  matunitlindflem1  22987  matunitlindflem2  22988  cpmatmcllem  23029  tgcl  23280  0ntr  23382  innei  23436  neitr  23491  ordtrest2lem  23514  cncnp  23591  cnnei  23593  2ndcdisj  23768  dislly  23809  dissnlocfin  23841  kgenss  23855  ptcnplem  23933  ptcnp  23934  ptcn  23939  cnmpt2k  24000  qtoprest  24029  kqt0lem  24048  isr0  24049  kqreglem1  24053  trfilss  24201  isufil2  24220  ufileu  24231  hausflim  24293  cnextcn  24379  symgtgp  24418  tsmssubm  24455  tsmsxplem1  24465  ustfilxp  24525  ustuqtop0  24552  elbl2ps  24701  elbl2  24702  nrginvrcn  25004  nmoix  25041  nmoleub  25043  cncfco  25221  icccvx  25264  iscmet3  25607  rrxmet  25722  ovolfioo  25781  ovolficc  25782  ovolicc2lem4  25834  iunmbl2  25871  dyadmax  25912  mbfsup  25978  mbflimsup  25980  mbflim  25982  itg1addlem4  26013  mbfi1flimlem  26036  itg2monolem1  26064  itg2mono  26067  itg2i1fseqle  26068  itg2i1fseq  26069  itg2addlem  26072  itg2gt0  26074  itg2cnlem1  26075  itgfsum  26140  cnlimc  26201  dvlip2  26308  itgsubst  26362  plyeq0lem  26522  plypf1  26524  dvtaylp  26690  ulmcaulem  26714  ulmcau  26715  ulmcn  26719  ulmdvlem3  26722  mtest  26724  pserulm  26742  pserdvlem2  26748  logdivlt  26942  advlogexp  26976  cxpexp  26989  cxpcl  26995  xrlimcnp  27289  basellem4  27404  logexprlim  27545  dchrsum2  27588  sumdchr2  27590  rpvmasum2  27832  pntrsumbnd2  27887  pntleml  27931  noreson  28010  z12zsodd  28861  tglineeltr  29092  plngrotlem2  29259  brbtwn2  29476  colinearalglem4  29480  axeuclidlem  29533  axcontlem8  29542  axcontlem10  29544  grpoidinvlem3  31101  grpoideu  31104  grpoinveu  31114  nmcvcn  31290  nmounbi  31371  blocnilem  31399  ubthlem1  31465  h2hlm  31575  ocsh  31878  brafnmul  32546  kbpj  32551  nmcexi  32621  lnconi  32628  riesz1  32660  mdbr2  32891  mdsl0  32905  mdslmd3i  32927  csmdsymi  32929  atcvatlem  32980  chirredlem1  32985  chirredi  32989  cdj3lem2b  33032  xrge0infss  33345  mgcmntco  33548  lmodvslmhm  33604  suppgsumssiun  33626  gsumwrd2dccatlem  33631  submarchi  33740  dvdsruasso  33933  grplsm0l  33947  ssmxidllem  33991  rprmndvdsru  34054  r1plmhm  34134  mplvrpmmhm  34171  mplvrpmrhm  34172  esplyfval1  34198  lindsunlem  34249  lindsun  34250  fldextrspunlsplem  34298  extdgfialglem2  34318  madjusmdetlem2  34453  zarcmplem  34506  ordtrest2NEWlem  34547  voliune  34855  fsum2dsub  35229  circlemeth  35262  bnj110  35481  cvxsconn  35987  btwnouttr2  36767  cgrxfr  36800  btwnxfr  36801  lineext  36821  segcon2  36850  brsegle2  36854  seglecgr12im  36855  segletr  36859  broutsideof3  36871  outsideofeu  36876  lineunray  36892  lineelsb2  36893  nmulrid  36926  neibastop3  37130  ttcmin  37264  bj-imdiridlem  38086  isbasisrelowllem1  38258  isbasisrelowllem2  38259  fvineqsneu  38314  unccur  38506  fin2solem  38509  lindsadd  38516  poimirlem4  38522  poimirlem6  38524  poimirlem7  38525  poimirlem22  38540  poimirlem23  38541  poimirlem25  38543  poimirlem26  38544  poimirlem28  38546  poimirlem30  38548  poimirlem31  38549  poimirlem32  38550  poimir  38551  broucube  38552  heicant  38553  mblfinlem3  38557  volsupnfl  38563  itg2addnclem  38569  itg2addnclem2  38570  itg2addnclem3  38571  ftc1anclem1  38591  ftc1anclem5  38595  ftc1anclem6  38596  ftc1anc  38599  unirep  38628  filbcmb  38654  fzmul  38655  fdc  38659  nninfnub  38665  isbnd2  38697  bndss  38700  prdsbnd  38707  prdstotbnd  38708  ismtyres  38722  rrnmet  38743  rrncmslem  38746  rrnequiv  38749  ghomco  38805  grpokerinj  38807  rngonegmn1l  38855  isdrngo2  38872  rngoisocnv  38895  divrngidl  38942  intidl  38943  unichnidl  38945  prnc  38981  isfldidl  38982  cvrexchlem  40456  ps-2  40515  3atnelvolN  40623  dib1dim  42202  dib1dim2  42205  expeqidd  43362  evlselv  43597  fsuppind  43598  mzpindd  43736  dvdsabsmod0  43973  radcnvrat  45283  expgrowth  45304  modelac8prim  45960  fnchoice  46015  infxrbnd2  46349  infleinflem2  46351  xrralrecnnge  46370  limsuppnfdlem  46680  icccncfext  46866  dvnmul  46922  dvnprodlem2  46926  stoweidlem17  46996  stoweidlem30  47009  stoweidlem38  47017  stoweidlem42  47021  stoweidlem44  47023  fourierdlem31  47117  fourierdlem73  47158  fourierdlem74  47159  fourierdlem75  47160  fourierdlem83  47168  fourierdlem94  47179  fourierdlem113  47198  etransclem4  47217  hoicvr  47527  iinhoiicclem  47652  iccvonmbllem  47657  smfsuplem1  47790  smfsupdmmbllem  47823  smfinfdmmbllem  47827  itsclquadeu  49858  aacllem  50908  veroquadmodzerod  50953