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  5628  ordintdif  6374  ordunisssuc  6431  fssres  6706  dffv2  6935  isocnv  7285  f1oiso  7306  f1ocnvfv3  7362  fiunlem  7895  onfununi  8281  oev2  8458  oaordi  8481  oaass  8496  omlimcl  8513  odi  8514  omass  8515  oewordri  8528  oelim2  8531  oeoa  8533  oeoe  8535  nnaordi  8554  omabs  8587  eceqoveq  8769  mapxpen  9081  mapdom2  9086  findcard  9098  dif1ennnALT  9187  fimax2g  9196  isfinite2  9208  fimin2g  9412  rankval3b  9750  isf32lem9  10283  fin1a2s  10336  zornn0g  10427  gchen1  10548  gchen2  10549  intwun  10658  suplem2pr  10976  recexsrlem  11026  axpre-sup  11092  axsup  11221  dedekind  11309  recextlem2  11781  divne0  11821  dfinfre  12137  qreccl  12919  xrlttr  13091  xaddf  13176  xrsupsslem  13259  xrinfmsslem  13260  supxr2  13266  supxrunb1  13271  supxrbnd1  13273  supxrbnd2  13274  modid  13855  seqof  14021  cau3lem  15317  lo1bdd2  15486  o1co  15548  rlimcn3  15552  climcn1  15554  climcn2  15555  rlimsqzlem  15611  caucvgb  15642  fsumrlim  15774  fsumo1  15775  ntrivcvg  15862  rplpwr  16527  dvdssq  16536  nn0seqcvgd  16539  lcmgcdlem  16575  isprm6  16684  phiprmpw  16746  pcneg  16845  prmpwdvds  16875  4sqlem19  16934  0ramcl  16994  imasleval  17505  catpropd  17675  funcres2c  17870  initoeu2  17983  oduprs  18266  latdisdlem  18462  acsfiindd  18519  dirtr  18568  chnind  18587  mndpsuppss  18733  mndind  18796  grpinveu  18950  mulgnn0subcl  19063  mulgsubcl  19064  mhmmulg  19091  cycsubm  19177  cycsubgcl  19181  cycsubgss  19182  ghmmulg  19203  odf1  19537  dfod2  19539  gexdvds2  19560  sylow2blem3  19597  frgpup1  19750  iscyggen2  19856  iscyg3  19861  prdsgsum  19956  ringrghm  20294  pwsgprod  20309  dvdsrcl2  20346  crngunit  20358  dvdsrpropd  20396  lss1d  20958  quscrng  21281  mulgghm2  21456  frgpcyg  21553  ip0r  21617  isphld  21634  frlmgsum  21752  uvcresum  21773  psdmul  22132  coe1tmmul  22242  mdetdiagid  22565  cpmatmcllem  22683  tgcl  22934  0ntr  23036  innei  23090  neitr  23145  ordtrest2lem  23168  cncnp  23245  cnnei  23247  2ndcdisj  23421  dislly  23462  dissnlocfin  23494  kgenss  23508  ptcnplem  23586  ptcnp  23587  ptcn  23592  cnmpt2k  23653  qtoprest  23682  kqt0lem  23701  isr0  23702  kqreglem1  23706  trfilss  23854  isufil2  23873  ufileu  23884  hausflim  23946  cnextcn  24032  symgtgp  24071  tsmssubm  24108  tsmsxplem1  24118  ustfilxp  24178  ustuqtop0  24205  elbl2ps  24354  elbl2  24355  nrginvrcn  24657  nmoix  24694  nmoleub  24696  cncfco  24874  icccvx  24917  iscmet3  25260  rrxmet  25375  ovolfioo  25434  ovolficc  25435  ovolicc2lem4  25487  iunmbl2  25524  dyadmax  25565  mbfsup  25631  mbflimsup  25633  mbflim  25635  itg1addlem4  25666  mbfi1flimlem  25689  itg2monolem1  25717  itg2mono  25720  itg2i1fseqle  25721  itg2i1fseq  25722  itg2addlem  25725  itg2gt0  25727  itg2cnlem1  25728  itgfsum  25794  cnlimc  25855  dvlip2  25962  itgsubst  26016  plyeq0lem  26175  plypf1  26177  dvtaylp  26335  ulmcaulem  26359  ulmcau  26360  ulmcn  26364  ulmdvlem3  26367  mtest  26369  pserulm  26387  pserdvlem2  26393  logdivlt  26585  advlogexp  26619  cxpexp  26632  cxpcl  26638  xrlimcnp  26932  basellem4  27047  logexprlim  27188  dchrsum2  27231  sumdchr2  27233  rpvmasum2  27475  pntrsumbnd2  27530  pntleml  27574  noreson  27624  z12zsodd  28474  tglineeltr  28699  brbtwn2  28974  colinearalglem4  28978  axeuclidlem  29031  axcontlem8  29040  axcontlem10  29042  grpoidinvlem3  30577  grpoideu  30580  grpoinveu  30590  nmcvcn  30766  nmounbi  30847  blocnilem  30875  ubthlem1  30941  h2hlm  31051  ocsh  31354  brafnmul  32022  kbpj  32027  nmcexi  32097  lnconi  32104  riesz1  32136  mdbr2  32367  mdsl0  32381  mdslmd3i  32403  csmdsymi  32405  atcvatlem  32456  chirredlem1  32461  chirredi  32465  cdj3lem2b  32508  xrge0infss  32833  mgcmntco  33054  lmodvslmhm  33111  suppgsumssiun  33133  gsumwrd2dccatlem  33138  submarchi  33247  dvdsruasso  33445  grplsm0l  33463  ssdifidllem  33516  ssdifidlprm  33518  ssmxidllem  33533  rprmndvdsru  33589  r1plmhm  33670  mplvrpmmhm  33690  mplvrpmrhm  33691  esplyfval1  33717  lindsunlem  33768  lindsun  33769  fldextrspunlsplem  33817  extdgfialglem2  33837  madjusmdetlem2  33972  zarcmplem  34025  ordtrest2NEWlem  34066  voliune  34373  fsum2dsub  34751  circlemeth  34784  bnj110  35000  cvxsconn  35425  btwnouttr2  36204  cgrxfr  36237  btwnxfr  36238  lineext  36258  segcon2  36287  brsegle2  36291  seglecgr12im  36292  segletr  36296  broutsideof3  36308  outsideofeu  36313  lineunray  36329  lineelsb2  36330  neibastop3  36544  ttcmin  36678  mh-inf3f1  36723  bj-imdiridlem  37499  isbasisrelowllem1  37671  isbasisrelowllem2  37672  fvineqsneu  37727  unccur  37924  fin2solem  37927  lindsadd  37934  matunitlindflem1  37937  matunitlindflem2  37938  poimirlem4  37945  poimirlem6  37947  poimirlem7  37948  poimirlem22  37963  poimirlem23  37964  poimirlem25  37966  poimirlem26  37967  poimirlem28  37969  poimirlem30  37971  poimirlem31  37972  poimirlem32  37973  poimir  37974  broucube  37975  heicant  37976  mblfinlem3  37980  volsupnfl  37986  itg2addnclem  37992  itg2addnclem2  37993  itg2addnclem3  37994  ftc1anclem1  38014  ftc1anclem5  38018  ftc1anclem6  38019  ftc1anc  38022  unirep  38035  filbcmb  38061  fzmul  38062  fdc  38066  nninfnub  38072  isbnd2  38104  bndss  38107  prdsbnd  38114  prdstotbnd  38115  ismtyres  38129  rrnmet  38150  rrncmslem  38153  rrnequiv  38156  ghomco  38212  grpokerinj  38214  rngonegmn1l  38262  isdrngo2  38279  rngoisocnv  38302  divrngidl  38349  intidl  38350  unichnidl  38352  prnc  38388  isfldidl  38389  cvrexchlem  39865  ps-2  39924  3atnelvolN  40032  dib1dim  41611  dib1dim2  41614  f1o2d2  42674  expeqidd  42757  evlselv  43020  fsuppind  43023  mzpindd  43178  dvdsabsmod0  43415  radcnvrat  44741  expgrowth  44762  modelac8prim  45419  fnchoice  45460  infxrbnd2  45798  infleinflem2  45800  xrralrecnnge  45819  limsuppnfdlem  46129  icccncfext  46315  dvnmul  46371  dvnprodlem2  46375  stoweidlem17  46445  stoweidlem30  46458  stoweidlem38  46466  stoweidlem42  46470  stoweidlem44  46472  fourierdlem31  46566  fourierdlem73  46607  fourierdlem74  46608  fourierdlem75  46609  fourierdlem83  46617  fourierdlem94  46628  fourierdlem113  46647  etransclem4  46666  hoicvr  46976  iinhoiicclem  47101  iccvonmbllem  47106  smfsuplem1  47239  smfsupdmmbllem  47272  smfinfdmmbllem  47276  itsclquadeu  49253  aacllem  50276