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  823  wereu2  5685  ordintdif  6435  ordunisssuc  6491  fssres  6774  dffv2  7003  isocnv  7349  f1oiso  7370  f1ocnvfv3  7425  fiunlem  7964  onfununi  8379  oev2  8559  oaordi  8582  oaass  8597  omlimcl  8614  odi  8615  omass  8616  oewordri  8628  oelim2  8631  oeoa  8633  oeoe  8635  nnaordi  8654  omabs  8687  eceqoveq  8860  mapxpen  9181  mapdom2  9186  findcard  9201  dif1ennnALT  9308  fimax2g  9319  isfinite2  9331  fimin2g  9534  rankval3b  9863  isf32lem9  10398  fin1a2s  10451  zornn0g  10542  gchen1  10662  gchen2  10663  intwun  10772  suplem2pr  11090  recexsrlem  11140  axpre-sup  11206  axsup  11333  dedekind  11421  recextlem2  11891  divne0  11931  dfinfre  12246  qreccl  13008  xrlttr  13178  xaddf  13262  xrsupsslem  13345  xrinfmsslem  13346  supxr2  13352  supxrunb1  13357  supxrbnd1  13359  supxrbnd2  13360  modid  13932  seqof  14096  cau3lem  15389  lo1bdd2  15556  o1co  15618  rlimcn3  15622  climcn1  15624  climcn2  15625  rlimsqzlem  15681  caucvgb  15712  fsumrlim  15843  fsumo1  15844  ntrivcvg  15929  rplpwr  16591  dvdssq  16600  nn0seqcvgd  16603  lcmgcdlem  16639  isprm6  16747  phiprmpw  16809  pcneg  16907  prmpwdvds  16937  4sqlem19  16996  0ramcl  17056  imasleval  17587  catpropd  17753  funcres2c  17954  initoeu2  18069  oduprs  18357  latdisdlem  18553  acsfiindd  18610  dirtr  18659  mndpsuppss  18790  mndind  18853  grpinveu  19004  mulgnn0subcl  19117  mulgsubcl  19118  mhmmulg  19145  cycsubm  19232  cycsubgcl  19236  cycsubgss  19237  ghmmulg  19258  odf1  19594  dfod2  19596  gexdvds2  19617  sylow2blem3  19654  frgpup1  19807  iscyggen2  19913  iscyg3  19918  prdsgsum  20013  ringrghm  20326  dvdsrcl2  20382  crngunit  20394  dvdsrpropd  20432  lss1d  20978  quscrng  21310  mulgghm2  21504  frgpcyg  21609  ip0r  21672  isphld  21689  frlmgsum  21809  uvcresum  21830  psdmul  22187  coe1tmmul  22295  mdetdiagid  22621  cpmatmcllem  22739  tgcl  22991  0ntr  23094  innei  23148  neitr  23203  ordtrest2lem  23226  cncnp  23303  cnnei  23305  2ndcdisj  23479  dislly  23520  dissnlocfin  23552  kgenss  23566  ptcnplem  23644  ptcnp  23645  ptcn  23650  cnmpt2k  23711  qtoprest  23740  kqt0lem  23759  isr0  23760  kqreglem1  23764  trfilss  23912  isufil2  23931  ufileu  23942  hausflim  24004  cnextcn  24090  symgtgp  24129  tsmssubm  24166  tsmsxplem1  24176  ustfilxp  24236  ustuqtop0  24264  elbl2ps  24414  elbl2  24415  nrginvrcn  24728  nmoix  24765  nmoleub  24767  cncfco  24946  icccvx  24994  iscmet3  25340  rrxmet  25455  ovolfioo  25515  ovolficc  25516  ovolicc2lem4  25568  iunmbl2  25605  dyadmax  25646  mbfsup  25712  mbflimsup  25714  mbflim  25716  itg1addlem4  25747  itg1addlem4OLD  25748  mbfi1flimlem  25771  itg2monolem1  25799  itg2mono  25802  itg2i1fseqle  25803  itg2i1fseq  25804  itg2addlem  25807  itg2gt0  25809  itg2cnlem1  25810  itgfsum  25876  cnlimc  25937  dvlip2  26048  itgsubst  26104  plyeq0lem  26263  plypf1  26265  dvtaylp  26426  ulmcaulem  26451  ulmcau  26452  ulmcn  26456  ulmdvlem3  26459  mtest  26461  pserulm  26479  pserdvlem2  26486  logdivlt  26677  advlogexp  26711  cxpexp  26724  cxpcl  26730  xrlimcnp  27025  basellem4  27141  logexprlim  27283  dchrsum2  27326  sumdchr2  27328  rpvmasum2  27570  pntrsumbnd2  27625  pntleml  27669  noreson  27719  tglineeltr  28653  brbtwn2  28934  colinearalglem4  28938  axeuclidlem  28991  axcontlem8  29000  axcontlem10  29002  grpoidinvlem3  30534  grpoideu  30537  grpoinveu  30547  nmcvcn  30723  nmounbi  30804  blocnilem  30832  ubthlem1  30898  h2hlm  31008  ocsh  31311  brafnmul  31979  kbpj  31984  nmcexi  32054  lnconi  32061  riesz1  32093  mdbr2  32324  mdsl0  32338  mdslmd3i  32360  csmdsymi  32362  atcvatlem  32413  chirredlem1  32418  chirredi  32422  cdj3lem2b  32465  xrge0infss  32770  mgcmntco  32968  chnind  32984  lmodvslmhm  33035  gsumwrd2dccatlem  33051  submarchi  33175  dvdsruasso  33392  grplsm0l  33410  ssdifidllem  33463  ssdifidlprm  33465  ssmxidllem  33480  rprmndvdsru  33536  r1plmhm  33609  lindsunlem  33651  lindsun  33652  madjusmdetlem2  33788  zarcmplem  33841  ordtrest2NEWlem  33882  voliune  34209  fsum2dsub  34600  circlemeth  34633  bnj110  34850  cvxsconn  35227  btwnouttr2  36003  cgrxfr  36036  btwnxfr  36037  lineext  36057  segcon2  36086  brsegle2  36090  seglecgr12im  36091  segletr  36095  broutsideof3  36107  outsideofeu  36112  lineunray  36128  lineelsb2  36129  neibastop3  36344  bj-imdiridlem  37167  isbasisrelowllem1  37337  isbasisrelowllem2  37338  fvineqsneu  37393  unccur  37589  fin2solem  37592  lindsadd  37599  matunitlindflem1  37602  matunitlindflem2  37603  poimirlem4  37610  poimirlem6  37612  poimirlem7  37613  poimirlem22  37628  poimirlem23  37629  poimirlem25  37631  poimirlem26  37632  poimirlem28  37634  poimirlem30  37636  poimirlem31  37637  poimirlem32  37638  poimir  37639  broucube  37640  heicant  37641  mblfinlem3  37645  volsupnfl  37651  itg2addnclem  37657  itg2addnclem2  37658  itg2addnclem3  37659  ftc1anclem1  37679  ftc1anclem5  37683  ftc1anclem6  37684  ftc1anc  37687  unirep  37700  filbcmb  37726  fzmul  37727  fdc  37731  nninfnub  37737  isbnd2  37769  bndss  37772  prdsbnd  37779  prdstotbnd  37780  ismtyres  37794  rrnmet  37815  rrncmslem  37818  rrnequiv  37821  ghomco  37877  grpokerinj  37879  rngonegmn1l  37927  isdrngo2  37944  rngoisocnv  37967  divrngidl  38014  intidl  38015  unichnidl  38017  prnc  38053  isfldidl  38054  cvrexchlem  39401  ps-2  39460  3atnelvolN  39568  dib1dim  41147  dib1dim2  41150  f1o2d2  42252  expeqidd  42338  pwsgprod  42530  evlselv  42573  fsuppind  42576  mzpindd  42733  dvdsabsmod0  42975  radcnvrat  44309  expgrowth  44330  fnchoice  44966  infxrbnd2  45318  infleinflem2  45320  xrralrecnnge  45339  limsuppnfdlem  45656  icccncfext  45842  dvnmul  45898  dvnprodlem2  45902  stoweidlem17  45972  stoweidlem30  45985  stoweidlem38  45993  stoweidlem42  45997  stoweidlem44  45999  fourierdlem31  46093  fourierdlem73  46134  fourierdlem74  46135  fourierdlem75  46136  fourierdlem83  46144  fourierdlem94  46155  fourierdlem113  46174  etransclem4  46193  iinhoiicclem  46628  iccvonmbllem  46633  smfsuplem1  46766  smfsupdmmbllem  46799  smfinfdmmbllem  46803  itsclquadeu  48626  aacllem  49031