Theorem an32s 650

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 644	. 2 ⊢ (((𝜑 ∧ 𝜒) ∧ 𝜓) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒))
2		an32s.1	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
3	1, 2	sylbi 219	1 ⊢ (((𝜑 ∧ 𝜒) ∧ 𝜓) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  anass1rs  653  anabss1  664  wereu2  5554  ordintdif  6242  ordunisssuc  6295  fssres  6546  foco  6604  dffv2  6758  isocnv  7085  f1oiso  7106  f1ocnvfv3  7154  fiunlem  7645  onfununi  7980  oev2  8150  oaordi  8174  oaass  8189  omlimcl  8206  odi  8207  omass  8208  oewordri  8220  oelim2  8223  oeoa  8225  oeoe  8227  nnaordi  8246  omabs  8276  eceqoveq  8404  mapxpen  8685  mapdom2  8690  dif1en  8753  findcard  8759  fimax2g  8766  isfinite2  8778  fimin2g  8963  rankval3b  9257  isf32lem9  9785  fin1a2s  9838  zornn0g  9929  gchen1  10049  gchen2  10050  intwun  10159  suplem2pr  10477  recexsrlem  10527  axpre-sup  10593  axsup  10718  dedekind  10805  recextlem2  11273  divne0  11312  dfinfre  11624  qreccl  12371  xrlttr  12536  xaddf  12620  xrsupsslem  12703  xrinfmsslem  12704  supxr2  12710  supxrunb1  12715  supxrbnd1  12717  supxrbnd2  12718  modid  13267  seqof  13430  cau3lem  14716  lo1bdd2  14883  o1co  14945  rlimcn2  14949  climcn1  14950  climcn2  14951  rlimsqzlem  15007  caucvgb  15038  fsumrlim  15168  fsumo1  15169  ntrivcvg  15255  rplpwr  15909  dvdssq  15913  nn0seqcvgd  15916  lcmgcdlem  15952  isprm6  16060  phiprmpw  16115  pcneg  16212  prmpwdvds  16242  4sqlem19  16301  0ramcl  16361  imasleval  16816  catpropd  16981  funcres2c  17173  initoeu2  17278  acsfiindd  17789  latdisdlem  17801  dirtr  17848  mndind  17994  grpinveu  18140  mulgnn0subcl  18243  mulgsubcl  18244  mhmmulg  18270  cycsubm  18347  cycsubgcl  18351  cycsubgss  18352  ghmmulg  18372  odf1  18691  dfod2  18693  gexdvds2  18712  sylow2blem3  18749  frgpup1  18903  iscyggen2  19002  iscyg3  19007  prdsgsum  19103  ringrghm  19357  dvdsrcl2  19402  crngunit  19414  dvdsrpropd  19448  lss1d  19737  quscrng  20015  coe1tmmul  20447  mulgghm2  20646  frgpcyg  20722  ip0r  20783  isphld  20800  frlmgsum  20918  uvcresum  20939  mdetdiagid  21211  cpmatmcllem  21328  tgcl  21579  0ntr  21681  innei  21735  neitr  21790  ordtrest2lem  21813  cncnp  21890  cnnei  21892  2ndcdisj  22066  dislly  22107  dissnlocfin  22139  kgenss  22153  ptcnplem  22231  ptcnp  22232  ptcn  22237  cnmpt2k  22298  qtoprest  22327  kqt0lem  22346  isr0  22347  kqreglem1  22351  trfilss  22499  isufil2  22518  ufileu  22529  hausflim  22591  cnextcn  22677  symgtgp  22716  tsmssubm  22753  tsmsxplem1  22763  ustfilxp  22823  ustuqtop0  22851  elbl2ps  23001  elbl2  23002  nrginvrcn  23303  nmoix  23340  nmoleub  23342  cncfco  23517  icccvx  23556  iscmet3  23898  rrxmet  24013  ovolfioo  24070  ovolficc  24071  ovolicc2lem4  24123  iunmbl2  24160  dyadmax  24201  mbfsup  24267  mbflimsup  24269  mbflim  24271  itg1addlem4  24302  mbfi1flimlem  24325  itg2monolem1  24353  itg2mono  24356  itg2i1fseqle  24357  itg2i1fseq  24358  itg2addlem  24361  itg2gt0  24363  itg2cnlem1  24364  itgfsum  24429  cnlimc  24488  dvlip2  24594  itgsubst  24648  plyeq0lem  24802  plypf1  24804  dvtaylp  24960  ulmcaulem  24984  ulmcau  24985  ulmcn  24989  ulmdvlem3  24992  mtest  24994  pserulm  25012  pserdvlem2  25018  logdivlt  25206  advlogexp  25240  cxpexp  25253  cxpcl  25259  xrlimcnp  25548  basellem4  25663  logexprlim  25803  dchrsum2  25846  sumdchr2  25848  rpvmasum2  26090  pntrsumbnd2  26145  pntleml  26189  tglineeltr  26419  brbtwn2  26693  colinearalglem4  26697  axeuclidlem  26750  axcontlem8  26759  axcontlem10  26761  grpoidinvlem3  28285  grpoideu  28288  grpoinveu  28298  nmcvcn  28474  nmounbi  28555  blocnilem  28583  ubthlem1  28649  h2hlm  28759  ocsh  29062  brafnmul  29730  kbpj  29735  nmcexi  29805  lnconi  29812  riesz1  29844  mdbr2  30075  mdsl0  30089  mdslmd3i  30111  csmdsymi  30113  atcvatlem  30164  chirredlem1  30169  chirredi  30173  cdj3lem2b  30216  xrge0infss  30486  oduprs  30645  lmodvslmhm  30690  submarchi  30817  ssmxidllem  30980  lindsunlem  31022  lindsun  31023  madjusmdetlem2  31095  ordtrest2NEWlem  31167  voliune  31490  fsum2dsub  31880  circlemeth  31913  bnj110  32132  cvxsconn  32492  noreson  33169  btwnouttr2  33485  cgrxfr  33518  btwnxfr  33519  lineext  33539  segcon2  33568  brsegle2  33572  seglecgr12im  33573  segletr  33577  broutsideof3  33589  outsideofeu  33594  lineunray  33610  lineelsb2  33611  neibastop3  33712  isbasisrelowllem1  34638  isbasisrelowllem2  34639  fvineqsneu  34694  unccur  34877  fin2solem  34880  lindsadd  34887  matunitlindflem1  34890  matunitlindflem2  34891  poimirlem4  34898  poimirlem6  34900  poimirlem7  34901  poimirlem22  34916  poimirlem23  34917  poimirlem25  34919  poimirlem26  34920  poimirlem28  34922  poimirlem30  34924  poimirlem31  34925  poimirlem32  34926  poimir  34927  broucube  34928  heicant  34929  mblfinlem3  34933  volsupnfl  34939  itg2addnclem  34945  itg2addnclem2  34946  itg2addnclem3  34947  ftc1anclem1  34969  ftc1anclem5  34973  ftc1anclem6  34974  ftc1anc  34977  unirep  34990  filbcmb  35017  fzmul  35018  fdc  35022  nninfnub  35028  isbnd2  35063  bndss  35066  prdsbnd  35073  prdstotbnd  35074  ismtyres  35088  rrnmet  35109  rrncmslem  35112  rrnequiv  35115  ghomco  35171  grpokerinj  35173  rngonegmn1l  35221  isdrngo2  35238  rngoisocnv  35261  divrngidl  35308  intidl  35309  unichnidl  35311  prnc  35347  isfldidl  35348  cvrexchlem  36557  ps-2  36616  3atnelvolN  36724  dib1dim  38303  dib1dim2  38306  mzpindd  39350  dvdsabsmod0  39591  radcnvrat  40653  expgrowth  40674  fnchoice  41293  infxrbnd2  41644  infleinflem2  41646  xrralrecnnge  41669  limsuppnfdlem  41989  icccncfext  42177  dvnmul  42235  dvnprodlem2  42239  stoweidlem17  42309  stoweidlem30  42322  stoweidlem38  42330  stoweidlem42  42334  stoweidlem44  42336  fourierdlem31  42430  fourierdlem73  42471  fourierdlem74  42472  fourierdlem75  42473  fourierdlem83  42481  fourierdlem94  42492  fourierdlem113  42511  etransclem4  42530  iinhoiicclem  42962  iccvonmbllem  42967  smfsuplem1  43092  mndpsuppss  44426  itsclquadeu  44771  aacllem  44909