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 216	1 ⊢ (((𝜑 ∧ 𝜒) ∧ 𝜓) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  anass1rs  653  anabss1  664  biadanid  821  wereu2  5628  ordintdif  6365  ordunisssuc  6420  fssres  6705  dffv2  6933  isocnv  7271  f1oiso  7292  f1ocnvfv3  7346  fiunlem  7866  onfununi  8279  oev2  8461  oaordi  8485  oaass  8500  omlimcl  8517  odi  8518  omass  8519  oewordri  8531  oelim2  8534  oeoa  8536  oeoe  8538  nnaordi  8557  omabs  8589  eceqoveq  8719  mapxpen  9045  mapdom2  9050  findcard  9065  dif1ennnALT  9179  fimax2g  9191  isfinite2  9203  fimin2g  9391  rankval3b  9720  isf32lem9  10255  fin1a2s  10308  zornn0g  10399  gchen1  10519  gchen2  10520  intwun  10629  suplem2pr  10947  recexsrlem  10997  axpre-sup  11063  axsup  11188  dedekind  11276  recextlem2  11744  divne0  11783  dfinfre  12094  qreccl  12848  xrlttr  13013  xaddf  13097  xrsupsslem  13180  xrinfmsslem  13181  supxr2  13187  supxrunb1  13192  supxrbnd1  13194  supxrbnd2  13195  modid  13755  seqof  13919  cau3lem  15193  lo1bdd2  15360  o1co  15422  rlimcn3  15426  climcn1  15428  climcn2  15429  rlimsqzlem  15487  caucvgb  15518  fsumrlim  15650  fsumo1  15651  ntrivcvg  15736  rplpwr  16392  dvdssq  16397  nn0seqcvgd  16400  lcmgcdlem  16436  isprm6  16544  phiprmpw  16602  pcneg  16700  prmpwdvds  16730  4sqlem19  16789  0ramcl  16849  imasleval  17377  catpropd  17543  funcres2c  17742  initoeu2  17856  latdisdlem  18339  acsfiindd  18396  dirtr  18445  mndind  18592  grpinveu  18739  mulgnn0subcl  18842  mulgsubcl  18843  mhmmulg  18870  cycsubm  18948  cycsubgcl  18952  cycsubgss  18953  ghmmulg  18973  odf1  19297  dfod2  19299  gexdvds2  19320  sylow2blem3  19357  frgpup1  19510  iscyggen2  19611  iscyg3  19616  prdsgsum  19711  ringrghm  19976  dvdsrcl2  20026  crngunit  20038  dvdsrpropd  20072  lss1d  20371  quscrng  20657  mulgghm2  20844  frgpcyg  20927  ip0r  20988  isphld  21005  frlmgsum  21125  uvcresum  21146  coe1tmmul  21594  mdetdiagid  21895  cpmatmcllem  22013  tgcl  22265  0ntr  22368  innei  22422  neitr  22477  ordtrest2lem  22500  cncnp  22577  cnnei  22579  2ndcdisj  22753  dislly  22794  dissnlocfin  22826  kgenss  22840  ptcnplem  22918  ptcnp  22919  ptcn  22924  cnmpt2k  22985  qtoprest  23014  kqt0lem  23033  isr0  23034  kqreglem1  23038  trfilss  23186  isufil2  23205  ufileu  23216  hausflim  23278  cnextcn  23364  symgtgp  23403  tsmssubm  23440  tsmsxplem1  23450  ustfilxp  23510  ustuqtop0  23538  elbl2ps  23688  elbl2  23689  nrginvrcn  24002  nmoix  24039  nmoleub  24041  cncfco  24216  icccvx  24259  iscmet3  24603  rrxmet  24718  ovolfioo  24777  ovolficc  24778  ovolicc2lem4  24830  iunmbl2  24867  dyadmax  24908  mbfsup  24974  mbflimsup  24976  mbflim  24978  itg1addlem4  25009  itg1addlem4OLD  25010  mbfi1flimlem  25033  itg2monolem1  25061  itg2mono  25064  itg2i1fseqle  25065  itg2i1fseq  25066  itg2addlem  25069  itg2gt0  25071  itg2cnlem1  25072  itgfsum  25137  cnlimc  25198  dvlip2  25305  itgsubst  25359  plyeq0lem  25517  plypf1  25519  dvtaylp  25675  ulmcaulem  25699  ulmcau  25700  ulmcn  25704  ulmdvlem3  25707  mtest  25709  pserulm  25727  pserdvlem2  25733  logdivlt  25922  advlogexp  25956  cxpexp  25969  cxpcl  25975  xrlimcnp  26264  basellem4  26379  logexprlim  26519  dchrsum2  26562  sumdchr2  26564  rpvmasum2  26806  pntrsumbnd2  26861  pntleml  26905  noreson  26954  tglineeltr  27418  brbtwn2  27699  colinearalglem4  27703  axeuclidlem  27756  axcontlem8  27765  axcontlem10  27767  grpoidinvlem3  29293  grpoideu  29296  grpoinveu  29306  nmcvcn  29482  nmounbi  29563  blocnilem  29591  ubthlem1  29657  h2hlm  29767  ocsh  30070  brafnmul  30738  kbpj  30743  nmcexi  30813  lnconi  30820  riesz1  30852  mdbr2  31083  mdsl0  31097  mdslmd3i  31119  csmdsymi  31121  atcvatlem  31172  chirredlem1  31177  chirredi  31181  cdj3lem2b  31224  xrge0infss  31507  oduprs  31666  mgcmntco  31696  lmodvslmhm  31734  submarchi  31864  grplsm0l  32026  ssmxidllem  32076  lindsunlem  32155  lindsun  32156  madjusmdetlem2  32237  zarcmplem  32290  ordtrest2NEWlem  32331  voliune  32656  fsum2dsub  33048  circlemeth  33081  bnj110  33298  cvxsconn  33665  btwnouttr2  34539  cgrxfr  34572  btwnxfr  34573  lineext  34593  segcon2  34622  brsegle2  34626  seglecgr12im  34627  segletr  34631  broutsideof3  34643  outsideofeu  34648  lineunray  34664  lineelsb2  34665  neibastop3  34766  bj-imdiridlem  35588  isbasisrelowllem1  35758  isbasisrelowllem2  35759  fvineqsneu  35814  unccur  35993  fin2solem  35996  lindsadd  36003  matunitlindflem1  36006  matunitlindflem2  36007  poimirlem4  36014  poimirlem6  36016  poimirlem7  36017  poimirlem22  36032  poimirlem23  36033  poimirlem25  36035  poimirlem26  36036  poimirlem28  36038  poimirlem30  36040  poimirlem31  36041  poimirlem32  36042  poimir  36043  broucube  36044  heicant  36045  mblfinlem3  36049  volsupnfl  36055  itg2addnclem  36061  itg2addnclem2  36062  itg2addnclem3  36063  ftc1anclem1  36083  ftc1anclem5  36087  ftc1anclem6  36088  ftc1anc  36091  unirep  36104  filbcmb  36131  fzmul  36132  fdc  36136  nninfnub  36142  isbnd2  36174  bndss  36177  prdsbnd  36184  prdstotbnd  36185  ismtyres  36199  rrnmet  36220  rrncmslem  36223  rrnequiv  36226  ghomco  36282  grpokerinj  36284  rngonegmn1l  36332  isdrngo2  36349  rngoisocnv  36372  divrngidl  36419  intidl  36420  unichnidl  36422  prnc  36458  isfldidl  36459  cvrexchlem  37814  ps-2  37873  3atnelvolN  37981  dib1dim  39560  dib1dim2  39563  pwsgprod  40658  fsuppind  40668  mzpindd  40972  dvdsabsmod0  41214  radcnvrat  42499  expgrowth  42520  fnchoice  43139  infxrbnd2  43502  infleinflem2  43504  xrralrecnnge  43524  limsuppnfdlem  43837  icccncfext  44023  dvnmul  44079  dvnprodlem2  44083  stoweidlem17  44153  stoweidlem30  44166  stoweidlem38  44174  stoweidlem42  44178  stoweidlem44  44180  fourierdlem31  44274  fourierdlem73  44315  fourierdlem74  44316  fourierdlem75  44317  fourierdlem83  44325  fourierdlem94  44336  fourierdlem113  44355  etransclem4  44374  iinhoiicclem  44809  iccvonmbllem  44814  smfsuplem1  44947  smfsupdmmbllem  44980  smfinfdmmbllem  44984  mndpsuppss  46342  itsclquadeu  46758  aacllem  47143