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  35216  btwnouttr2  35996  cgrxfr  36029  btwnxfr  36030  lineext  36050  segcon2  36079  brsegle2  36083  seglecgr12im  36084  segletr  36088  broutsideof3  36100  outsideofeu  36105  lineunray  36121  lineelsb2  36122  neibastop3  36336  bj-imdiridlem  37159  isbasisrelowllem1  37329  isbasisrelowllem2  37330  fvineqsneu  37385  unccur  37583  fin2solem  37586  lindsadd  37593  matunitlindflem1  37596  matunitlindflem2  37597  poimirlem4  37604  poimirlem6  37606  poimirlem7  37607  poimirlem22  37622  poimirlem23  37623  poimirlem25  37625  poimirlem26  37626  poimirlem28  37628  poimirlem30  37630  poimirlem31  37631  poimirlem32  37632  poimir  37633  broucube  37634  heicant  37635  mblfinlem3  37639  volsupnfl  37645  itg2addnclem  37651  itg2addnclem2  37652  itg2addnclem3  37653  ftc1anclem1  37673  ftc1anclem5  37677  ftc1anclem6  37678  ftc1anc  37681  unirep  37694  filbcmb  37720  fzmul  37721  fdc  37725  nninfnub  37731  isbnd2  37763  bndss  37766  prdsbnd  37773  prdstotbnd  37774  ismtyres  37788  rrnmet  37809  rrncmslem  37812  rrnequiv  37815  ghomco  37871  grpokerinj  37873  rngonegmn1l  37921  isdrngo2  37938  rngoisocnv  37961  divrngidl  38008  intidl  38009  unichnidl  38011  prnc  38047  isfldidl  38048  cvrexchlem  39398  ps-2  39457  3atnelvolN  39565  dib1dim  41144  dib1dim2  41147  f1o2d2  42206  expeqidd  42298  pwsgprod  42517  evlselv  42560  fsuppind  42563  mzpindd  42719  dvdsabsmod0  42960  radcnvrat  44287  expgrowth  44308  modelac8prim  44966  fnchoice  45007  infxrbnd2  45348  infleinflem2  45350  xrralrecnnge  45369  limsuppnfdlem  45682  icccncfext  45868  dvnmul  45924  dvnprodlem2  45928  stoweidlem17  45998  stoweidlem30  46011  stoweidlem38  46019  stoweidlem42  46023  stoweidlem44  46025  fourierdlem31  46119  fourierdlem73  46160  fourierdlem74  46161  fourierdlem75  46162  fourierdlem83  46170  fourierdlem94  46181  fourierdlem113  46200  etransclem4  46219  iinhoiicclem  46654  iccvonmbllem  46659  smfsuplem1  46792  smfsupdmmbllem  46825  smfinfdmmbllem  46829  itsclquadeu  48762  aacllem  49786