Theorem an32s 651

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

Syntax hints:   → wi 4   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  anass1rs  654  anabss1  665  wereu2  5516  ordintdif  6208  ordunisssuc  6261  fssres  6518  foco  6577  dffv2  6733  isocnv  7062  f1oiso  7083  f1ocnvfv3  7131  fiunlem  7625  onfununi  7961  oev2  8131  oaordi  8155  oaass  8170  omlimcl  8187  odi  8188  omass  8189  oewordri  8201  oelim2  8204  oeoa  8206  oeoe  8208  nnaordi  8227  omabs  8257  eceqoveq  8385  mapxpen  8667  mapdom2  8672  dif1en  8735  findcard  8741  fimax2g  8748  isfinite2  8760  fimin2g  8945  rankval3b  9239  isf32lem9  9772  fin1a2s  9825  zornn0g  9916  gchen1  10036  gchen2  10037  intwun  10146  suplem2pr  10464  recexsrlem  10514  axpre-sup  10580  axsup  10705  dedekind  10792  recextlem2  11260  divne0  11299  dfinfre  11609  qreccl  12356  xrlttr  12521  xaddf  12605  xrsupsslem  12688  xrinfmsslem  12689  supxr2  12695  supxrunb1  12700  supxrbnd1  12702  supxrbnd2  12703  modid  13259  seqof  13423  cau3lem  14706  lo1bdd2  14873  o1co  14935  rlimcn2  14939  climcn1  14940  climcn2  14941  rlimsqzlem  14997  caucvgb  15028  fsumrlim  15158  fsumo1  15159  ntrivcvg  15245  rplpwr  15897  dvdssq  15901  nn0seqcvgd  15904  lcmgcdlem  15940  isprm6  16048  phiprmpw  16103  pcneg  16200  prmpwdvds  16230  4sqlem19  16289  0ramcl  16349  imasleval  16806  catpropd  16971  funcres2c  17163  initoeu2  17268  acsfiindd  17779  latdisdlem  17791  dirtr  17838  mndind  17984  grpinveu  18130  mulgnn0subcl  18233  mulgsubcl  18234  mhmmulg  18260  cycsubm  18337  cycsubgcl  18341  cycsubgss  18342  ghmmulg  18362  odf1  18681  dfod2  18683  gexdvds2  18702  sylow2blem3  18739  frgpup1  18893  iscyggen2  18993  iscyg3  18998  prdsgsum  19094  ringrghm  19351  dvdsrcl2  19396  crngunit  19408  dvdsrpropd  19442  lss1d  19728  quscrng  20006  mulgghm2  20190  frgpcyg  20265  ip0r  20326  isphld  20343  frlmgsum  20461  uvcresum  20482  coe1tmmul  20906  mdetdiagid  21205  cpmatmcllem  21323  tgcl  21574  0ntr  21676  innei  21730  neitr  21785  ordtrest2lem  21808  cncnp  21885  cnnei  21887  2ndcdisj  22061  dislly  22102  dissnlocfin  22134  kgenss  22148  ptcnplem  22226  ptcnp  22227  ptcn  22232  cnmpt2k  22293  qtoprest  22322  kqt0lem  22341  isr0  22342  kqreglem1  22346  trfilss  22494  isufil2  22513  ufileu  22524  hausflim  22586  cnextcn  22672  symgtgp  22711  tsmssubm  22748  tsmsxplem1  22758  ustfilxp  22818  ustuqtop0  22846  elbl2ps  22996  elbl2  22997  nrginvrcn  23298  nmoix  23335  nmoleub  23337  cncfco  23512  icccvx  23555  iscmet3  23897  rrxmet  24012  ovolfioo  24071  ovolficc  24072  ovolicc2lem4  24124  iunmbl2  24161  dyadmax  24202  mbfsup  24268  mbflimsup  24270  mbflim  24272  itg1addlem4  24303  mbfi1flimlem  24326  itg2monolem1  24354  itg2mono  24357  itg2i1fseqle  24358  itg2i1fseq  24359  itg2addlem  24362  itg2gt0  24364  itg2cnlem1  24365  itgfsum  24430  cnlimc  24491  dvlip2  24598  itgsubst  24652  plyeq0lem  24807  plypf1  24809  dvtaylp  24965  ulmcaulem  24989  ulmcau  24990  ulmcn  24994  ulmdvlem3  24997  mtest  24999  pserulm  25017  pserdvlem2  25023  logdivlt  25212  advlogexp  25246  cxpexp  25259  cxpcl  25265  xrlimcnp  25554  basellem4  25669  logexprlim  25809  dchrsum2  25852  sumdchr2  25854  rpvmasum2  26096  pntrsumbnd2  26151  pntleml  26195  tglineeltr  26425  brbtwn2  26699  colinearalglem4  26703  axeuclidlem  26756  axcontlem8  26765  axcontlem10  26767  grpoidinvlem3  28289  grpoideu  28292  grpoinveu  28302  nmcvcn  28478  nmounbi  28559  blocnilem  28587  ubthlem1  28653  h2hlm  28763  ocsh  29066  brafnmul  29734  kbpj  29739  nmcexi  29809  lnconi  29816  riesz1  29848  mdbr2  30079  mdsl0  30093  mdslmd3i  30115  csmdsymi  30117  atcvatlem  30168  chirredlem1  30173  chirredi  30177  cdj3lem2b  30220  biadanid  30236  xrge0infss  30510  oduprs  30669  mgcmntco  30702  lmodvslmhm  30735  submarchi  30865  ssmxidllem  31049  lindsunlem  31108  lindsun  31109  madjusmdetlem2  31181  zarcmplem  31234  ordtrest2NEWlem  31275  voliune  31598  fsum2dsub  31988  circlemeth  32021  bnj110  32240  cvxsconn  32603  noreson  33280  btwnouttr2  33596  cgrxfr  33629  btwnxfr  33630  lineext  33650  segcon2  33679  brsegle2  33683  seglecgr12im  33684  segletr  33688  broutsideof3  33700  outsideofeu  33705  lineunray  33721  lineelsb2  33722  neibastop3  33823  bj-imdiridlem  34600  isbasisrelowllem1  34772  isbasisrelowllem2  34773  fvineqsneu  34828  unccur  35040  fin2solem  35043  lindsadd  35050  matunitlindflem1  35053  matunitlindflem2  35054  poimirlem4  35061  poimirlem6  35063  poimirlem7  35064  poimirlem22  35079  poimirlem23  35080  poimirlem25  35082  poimirlem26  35083  poimirlem28  35085  poimirlem30  35087  poimirlem31  35088  poimirlem32  35089  poimir  35090  broucube  35091  heicant  35092  mblfinlem3  35096  volsupnfl  35102  itg2addnclem  35108  itg2addnclem2  35109  itg2addnclem3  35110  ftc1anclem1  35130  ftc1anclem5  35134  ftc1anclem6  35135  ftc1anc  35138  unirep  35151  filbcmb  35178  fzmul  35179  fdc  35183  nninfnub  35189  isbnd2  35221  bndss  35224  prdsbnd  35231  prdstotbnd  35232  ismtyres  35246  rrnmet  35267  rrncmslem  35270  rrnequiv  35273  ghomco  35329  grpokerinj  35331  rngonegmn1l  35379  isdrngo2  35396  rngoisocnv  35419  divrngidl  35466  intidl  35467  unichnidl  35469  prnc  35505  isfldidl  35506  cvrexchlem  36715  ps-2  36774  3atnelvolN  36882  dib1dim  38461  dib1dim2  38464  fsuppind  39456  mzpindd  39687  dvdsabsmod0  39928  radcnvrat  41018  expgrowth  41039  fnchoice  41658  infxrbnd2  42001  infleinflem2  42003  xrralrecnnge  42026  limsuppnfdlem  42343  icccncfext  42529  dvnmul  42585  dvnprodlem2  42589  stoweidlem17  42659  stoweidlem30  42672  stoweidlem38  42680  stoweidlem42  42684  stoweidlem44  42686  fourierdlem31  42780  fourierdlem73  42821  fourierdlem74  42822  fourierdlem75  42823  fourierdlem83  42831  fourierdlem94  42842  fourierdlem113  42861  etransclem4  42880  iinhoiicclem  43312  iccvonmbllem  43317  smfsuplem1  43442  mndpsuppss  44773  itsclquadeu  45191  aacllem  45329