Theorem an32s 662

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

This theorem is referenced by:  anass1rs  665  anabss1  676  biadanid  832  wereu2  5640  ordintdif  6392  ordunisssuc  6449  fssres  6725  dffv2  6957  isocnv  7309  f1oiso  7330  f1ocnvfv3  7386  fiunlem  7918  mpof1o2d  8099  onfununi  8306  oev2  8486  oaordi  8509  oaass  8524  omlimcl  8541  odi  8542  omass  8543  oewordri  8556  oelim2  8559  oeoa  8561  oeoe  8563  nnaordi  8582  omabs  8615  eceqoveq  8798  mapxpen  9109  mapdom2  9114  findcard  9126  dif1ennnALT  9215  fimax2g  9224  isfinite2  9236  fimin2g  9439  rankval3b  9778  isf32lem9  10312  fin1a2s  10365  zornn0g  10456  gchen1  10577  gchen2  10578  intwun  10687  suplem2pr  11005  recexsrlem  11055  axpre-sup  11121  axsup  11252  dedekind  11340  recextlem2  11812  divne0  11851  dfinfre  12167  qreccl  12964  xrlttr  13136  xaddf  13221  xrsupsslem  13304  xrinfmsslem  13305  supxr2  13311  supxrunb1  13316  supxrbnd1  13318  supxrbnd2  13319  modid  13900  seqof  14066  cau3lem  15373  lo1bdd2  15542  o1co  15604  rlimcn3  15608  climcn1  15610  climcn2  15611  rlimsqzlem  15667  caucvgb  15698  fsumrlim  15830  fsumo1  15831  ntrivcvg  15918  rplpwr  16583  dvdssq  16592  nn0seqcvgd  16595  lcmgcdlem  16631  isprm6  16740  phiprmpw  16802  pcneg  16901  prmpwdvds  16931  4sqlem19  16990  0ramcl  17050  imasleval  17562  catpropd  17732  funcres2c  17927  initoeu2  18040  oduprs  18323  latdisdlem  18519  acsfiindd  18576  dirtr  18625  chnind  18644  mndpsuppss  18790  mndind  18853  grpinveu  19007  mulgnn0subcl  19120  mulgsubcl  19121  mhmmulg  19148  cycsubm  19234  cycsubgcl  19238  cycsubgss  19239  ghmmulg  19259  odf1  19593  dfod2  19595  gexdvds2  19616  sylow2blem3  19653  frgpup1  19806  iscyggen2  19912  iscyg3  19917  prdsgsum  20012  ringrghm  20350  pwsgprod  20365  dvdsrcl2  20402  crngunit  20414  dvdsrpropd  20452  lss1d  21018  quscrng  21341  mulgghm2  21516  frgpcyg  21613  ip0r  21677  isphld  21694  frlmgsum  21812  uvcresum  21833  psdmul  22219  coe1tmmul  22328  mdetdiagid  22648  cpmatmcllem  22766  tgcl  23017  0ntr  23119  innei  23173  neitr  23228  ordtrest2lem  23251  cncnp  23328  cnnei  23330  2ndcdisj  23504  dislly  23545  dissnlocfin  23577  kgenss  23591  ptcnplem  23669  ptcnp  23670  ptcn  23675  cnmpt2k  23736  qtoprest  23765  kqt0lem  23784  isr0  23785  kqreglem1  23789  trfilss  23937  isufil2  23956  ufileu  23967  hausflim  24029  cnextcn  24115  symgtgp  24154  tsmssubm  24191  tsmsxplem1  24201  ustfilxp  24261  ustuqtop0  24288  elbl2ps  24437  elbl2  24438  nrginvrcn  24740  nmoix  24777  nmoleub  24779  cncfco  24957  icccvx  25000  iscmet3  25343  rrxmet  25458  ovolfioo  25517  ovolficc  25518  ovolicc2lem4  25570  iunmbl2  25607  dyadmax  25648  mbfsup  25714  mbflimsup  25716  mbflim  25718  itg1addlem4  25749  mbfi1flimlem  25772  itg2monolem1  25800  itg2mono  25803  itg2i1fseqle  25804  itg2i1fseq  25805  itg2addlem  25808  itg2gt0  25810  itg2cnlem1  25811  itgfsum  25877  cnlimc  25938  dvlip2  26045  itgsubst  26099  plyeq0lem  26258  plypf1  26260  dvtaylp  26421  ulmcaulem  26445  ulmcau  26446  ulmcn  26450  ulmdvlem3  26453  mtest  26455  pserulm  26473  pserdvlem2  26479  logdivlt  26674  advlogexp  26708  cxpexp  26721  cxpcl  26727  xrlimcnp  27021  basellem4  27136  logexprlim  27277  dchrsum2  27320  sumdchr2  27322  rpvmasum2  27564  pntrsumbnd2  27619  pntleml  27663  noreson  27712  z12zsodd  28563  tglineeltr  28788  brbtwn2  29063  colinearalglem4  29067  axeuclidlem  29120  axcontlem8  29129  axcontlem10  29131  grpoidinvlem3  30666  grpoideu  30669  grpoinveu  30679  nmcvcn  30855  nmounbi  30936  blocnilem  30964  ubthlem1  31030  h2hlm  31140  ocsh  31443  brafnmul  32111  kbpj  32116  nmcexi  32186  lnconi  32193  riesz1  32225  mdbr2  32456  mdsl0  32470  mdslmd3i  32492  csmdsymi  32494  atcvatlem  32545  chirredlem1  32550  chirredi  32554  cdj3lem2b  32597  xrge0infss  32923  mgcmntco  33133  lmodvslmhm  33191  suppgsumssiun  33213  gsumwrd2dccatlem  33218  submarchi  33327  dvdsruasso  33532  grplsm0l  33550  ssdifidllem  33604  ssdifidlprm  33606  ssmxidllem  33622  rprmndvdsru  33686  r1plmhm  33767  mplvrpmmhm  33804  mplvrpmrhm  33805  esplyfval1  33831  lindsunlem  33882  lindsun  33883  fldextrspunlsplem  33931  extdgfialglem2  33951  madjusmdetlem2  34086  zarcmplem  34139  ordtrest2NEWlem  34180  voliune  34487  fsum2dsub  34862  circlemeth  34895  bnj110  35114  cvxsconn  35554  btwnouttr2  36333  cgrxfr  36366  btwnxfr  36367  lineext  36387  segcon2  36416  brsegle2  36420  seglecgr12im  36421  segletr  36425  broutsideof3  36437  outsideofeu  36442  lineunray  36458  lineelsb2  36459  neibastop3  36683  ttcmin  36817  mh-inf3f1  36862  bj-imdiridlem  37638  isbasisrelowllem1  37810  isbasisrelowllem2  37811  fvineqsneu  37866  unccur  38063  fin2solem  38066  lindsadd  38073  matunitlindflem1  38076  matunitlindflem2  38077  poimirlem4  38084  poimirlem6  38086  poimirlem7  38087  poimirlem22  38102  poimirlem23  38103  poimirlem25  38105  poimirlem26  38106  poimirlem28  38108  poimirlem30  38110  poimirlem31  38111  poimirlem32  38112  poimir  38113  broucube  38114  heicant  38115  mblfinlem3  38119  volsupnfl  38125  itg2addnclem  38131  itg2addnclem2  38132  itg2addnclem3  38133  ftc1anclem1  38153  ftc1anclem5  38157  ftc1anclem6  38158  ftc1anc  38161  unirep  38174  filbcmb  38200  fzmul  38201  fdc  38205  nninfnub  38211  isbnd2  38243  bndss  38246  prdsbnd  38253  prdstotbnd  38254  ismtyres  38268  rrnmet  38289  rrncmslem  38292  rrnequiv  38295  ghomco  38351  grpokerinj  38353  rngonegmn1l  38401  isdrngo2  38418  rngoisocnv  38441  divrngidl  38488  intidl  38489  unichnidl  38491  prnc  38527  isfldidl  38528  cvrexchlem  40004  ps-2  40063  3atnelvolN  40171  dib1dim  41750  dib1dim2  41753  expeqidd  42895  evlselv  43132  fsuppind  43133  mzpindd  43288  dvdsabsmod0  43525  radcnvrat  44851  expgrowth  44872  modelac8prim  45529  fnchoice  45570  infxrbnd2  45905  infleinflem2  45907  xrralrecnnge  45926  limsuppnfdlem  46236  icccncfext  46422  dvnmul  46478  dvnprodlem2  46482  stoweidlem17  46552  stoweidlem30  46565  stoweidlem38  46573  stoweidlem42  46577  stoweidlem44  46579  fourierdlem31  46673  fourierdlem73  46714  fourierdlem74  46715  fourierdlem75  46716  fourierdlem83  46724  fourierdlem94  46735  fourierdlem113  46754  etransclem4  46773  hoicvr  47083  iinhoiicclem  47208  iccvonmbllem  47213  smfsuplem1  47346  smfsupdmmbllem  47379  smfinfdmmbllem  47383  itsclquadeu  49360  aacllem  50383