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  822  wereu2  5616  ordintdif  6358  ordunisssuc  6415  fssres  6690  dffv2  6918  isocnv  7267  f1oiso  7288  f1ocnvfv3  7344  fiunlem  7877  onfununi  8264  oev2  8441  oaordi  8464  oaass  8479  omlimcl  8496  odi  8497  omass  8498  oewordri  8510  oelim2  8513  oeoa  8515  oeoe  8517  nnaordi  8536  omabs  8569  eceqoveq  8749  mapxpen  9060  mapdom2  9065  findcard  9077  dif1ennnALT  9166  fimax2g  9175  isfinite2  9187  fimin2g  9389  rankval3b  9722  isf32lem9  10255  fin1a2s  10308  zornn0g  10399  gchen1  10519  gchen2  10520  intwun  10629  suplem2pr  10947  recexsrlem  10997  axpre-sup  11063  axsup  11191  dedekind  11279  recextlem2  11751  divne0  11791  dfinfre  12106  qreccl  12870  xrlttr  13042  xaddf  13126  xrsupsslem  13209  xrinfmsslem  13210  supxr2  13216  supxrunb1  13221  supxrbnd1  13223  supxrbnd2  13224  modid  13800  seqof  13966  cau3lem  15262  lo1bdd2  15431  o1co  15493  rlimcn3  15497  climcn1  15499  climcn2  15500  rlimsqzlem  15556  caucvgb  15587  fsumrlim  15718  fsumo1  15719  ntrivcvg  15804  rplpwr  16469  dvdssq  16478  nn0seqcvgd  16481  lcmgcdlem  16517  isprm6  16625  phiprmpw  16687  pcneg  16786  prmpwdvds  16816  4sqlem19  16875  0ramcl  16935  imasleval  17445  catpropd  17615  funcres2c  17810  initoeu2  17923  oduprs  18206  latdisdlem  18402  acsfiindd  18459  dirtr  18508  mndpsuppss  18639  mndind  18702  grpinveu  18853  mulgnn0subcl  18966  mulgsubcl  18967  mhmmulg  18994  cycsubm  19081  cycsubgcl  19085  cycsubgss  19086  ghmmulg  19107  odf1  19441  dfod2  19443  gexdvds2  19464  sylow2blem3  19501  frgpup1  19654  iscyggen2  19760  iscyg3  19765  prdsgsum  19860  ringrghm  20198  dvdsrcl2  20251  crngunit  20263  dvdsrpropd  20301  lss1d  20866  quscrng  21190  mulgghm2  21383  frgpcyg  21480  ip0r  21544  isphld  21561  frlmgsum  21679  uvcresum  21700  psdmul  22051  coe1tmmul  22161  mdetdiagid  22485  cpmatmcllem  22603  tgcl  22854  0ntr  22956  innei  23010  neitr  23065  ordtrest2lem  23088  cncnp  23165  cnnei  23167  2ndcdisj  23341  dislly  23382  dissnlocfin  23414  kgenss  23428  ptcnplem  23506  ptcnp  23507  ptcn  23512  cnmpt2k  23573  qtoprest  23602  kqt0lem  23621  isr0  23622  kqreglem1  23626  trfilss  23774  isufil2  23793  ufileu  23804  hausflim  23866  cnextcn  23952  symgtgp  23991  tsmssubm  24028  tsmsxplem1  24038  ustfilxp  24098  ustuqtop0  24126  elbl2ps  24275  elbl2  24276  nrginvrcn  24578  nmoix  24615  nmoleub  24617  cncfco  24798  icccvx  24846  iscmet3  25191  rrxmet  25306  ovolfioo  25366  ovolficc  25367  ovolicc2lem4  25419  iunmbl2  25456  dyadmax  25497  mbfsup  25563  mbflimsup  25565  mbflim  25567  itg1addlem4  25598  mbfi1flimlem  25621  itg2monolem1  25649  itg2mono  25652  itg2i1fseqle  25653  itg2i1fseq  25654  itg2addlem  25657  itg2gt0  25659  itg2cnlem1  25660  itgfsum  25726  cnlimc  25787  dvlip2  25898  itgsubst  25954  plyeq0lem  26113  plypf1  26115  dvtaylp  26276  ulmcaulem  26301  ulmcau  26302  ulmcn  26306  ulmdvlem3  26309  mtest  26311  pserulm  26329  pserdvlem2  26336  logdivlt  26528  advlogexp  26562  cxpexp  26575  cxpcl  26581  xrlimcnp  26876  basellem4  26992  logexprlim  27134  dchrsum2  27177  sumdchr2  27179  rpvmasum2  27421  pntrsumbnd2  27476  pntleml  27520  noreson  27570  zs12zodd  28359  tglineeltr  28576  brbtwn2  28850  colinearalglem4  28854  axeuclidlem  28907  axcontlem8  28916  axcontlem10  28918  grpoidinvlem3  30450  grpoideu  30453  grpoinveu  30463  nmcvcn  30639  nmounbi  30720  blocnilem  30748  ubthlem1  30814  h2hlm  30924  ocsh  31227  brafnmul  31895  kbpj  31900  nmcexi  31970  lnconi  31977  riesz1  32009  mdbr2  32240  mdsl0  32254  mdslmd3i  32276  csmdsymi  32278  atcvatlem  32329  chirredlem1  32334  chirredi  32338  cdj3lem2b  32381  xrge0infss  32703  mgcmntco  32936  chnind  32953  lmodvslmhm  33003  gsumwrd2dccatlem  33019  submarchi  33128  dvdsruasso  33322  grplsm0l  33340  ssdifidllem  33393  ssdifidlprm  33395  ssmxidllem  33410  rprmndvdsru  33466  r1plmhm  33542  lindsunlem  33591  lindsun  33592  fldextrspunlsplem  33640  extdgfialglem2  33660  madjusmdetlem2  33795  zarcmplem  33848  ordtrest2NEWlem  33889  voliune  34196  fsum2dsub  34575  circlemeth  34608  bnj110  34825  cvxsconn  35220  btwnouttr2  36000  cgrxfr  36033  btwnxfr  36034  lineext  36054  segcon2  36083  brsegle2  36087  seglecgr12im  36088  segletr  36092  broutsideof3  36104  outsideofeu  36109  lineunray  36125  lineelsb2  36126  neibastop3  36340  bj-imdiridlem  37163  isbasisrelowllem1  37333  isbasisrelowllem2  37334  fvineqsneu  37389  unccur  37587  fin2solem  37590  lindsadd  37597  matunitlindflem1  37600  matunitlindflem2  37601  poimirlem4  37608  poimirlem6  37610  poimirlem7  37611  poimirlem22  37626  poimirlem23  37627  poimirlem25  37629  poimirlem26  37630  poimirlem28  37632  poimirlem30  37634  poimirlem31  37635  poimirlem32  37636  poimir  37637  broucube  37638  heicant  37639  mblfinlem3  37643  volsupnfl  37649  itg2addnclem  37655  itg2addnclem2  37656  itg2addnclem3  37657  ftc1anclem1  37677  ftc1anclem5  37681  ftc1anclem6  37682  ftc1anc  37685  unirep  37698  filbcmb  37724  fzmul  37725  fdc  37729  nninfnub  37735  isbnd2  37767  bndss  37770  prdsbnd  37777  prdstotbnd  37778  ismtyres  37792  rrnmet  37813  rrncmslem  37816  rrnequiv  37819  ghomco  37875  grpokerinj  37877  rngonegmn1l  37925  isdrngo2  37942  rngoisocnv  37965  divrngidl  38012  intidl  38013  unichnidl  38015  prnc  38051  isfldidl  38052  cvrexchlem  39402  ps-2  39461  3atnelvolN  39569  dib1dim  41148  dib1dim2  41151  f1o2d2  42210  expeqidd  42302  pwsgprod  42521  evlselv  42564  fsuppind  42567  mzpindd  42723  dvdsabsmod0  42964  radcnvrat  44291  expgrowth  44312  modelac8prim  44970  fnchoice  45011  infxrbnd2  45352  infleinflem2  45354  xrralrecnnge  45373  limsuppnfdlem  45686  icccncfext  45872  dvnmul  45928  dvnprodlem2  45932  stoweidlem17  46002  stoweidlem30  46015  stoweidlem38  46023  stoweidlem42  46027  stoweidlem44  46029  fourierdlem31  46123  fourierdlem73  46164  fourierdlem74  46165  fourierdlem75  46166  fourierdlem83  46174  fourierdlem94  46185  fourierdlem113  46204  etransclem4  46223  iinhoiicclem  46658  iccvonmbllem  46663  smfsuplem1  46796  smfsupdmmbllem  46829  smfinfdmmbllem  46833  itsclquadeu  48766  aacllem  49790