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  5635  ordintdif  6372  ordunisssuc  6428  fssres  6713  dffv2  6941  isocnv  7280  f1oiso  7301  f1ocnvfv3  7357  fiunlem  7879  onfununi  8292  oev2  8474  oaordi  8498  oaass  8513  omlimcl  8530  odi  8531  omass  8532  oewordri  8544  oelim2  8547  oeoa  8549  oeoe  8551  nnaordi  8570  omabs  8602  eceqoveq  8768  mapxpen  9094  mapdom2  9099  findcard  9114  dif1ennnALT  9228  fimax2g  9240  isfinite2  9252  fimin2g  9442  rankval3b  9771  isf32lem9  10306  fin1a2s  10359  zornn0g  10450  gchen1  10570  gchen2  10571  intwun  10680  suplem2pr  10998  recexsrlem  11048  axpre-sup  11114  axsup  11239  dedekind  11327  recextlem2  11795  divne0  11834  dfinfre  12145  qreccl  12903  xrlttr  13069  xaddf  13153  xrsupsslem  13236  xrinfmsslem  13237  supxr2  13243  supxrunb1  13248  supxrbnd1  13250  supxrbnd2  13251  modid  13811  seqof  13975  cau3lem  15251  lo1bdd2  15418  o1co  15480  rlimcn3  15484  climcn1  15486  climcn2  15487  rlimsqzlem  15545  caucvgb  15576  fsumrlim  15707  fsumo1  15708  ntrivcvg  15793  rplpwr  16449  dvdssq  16454  nn0seqcvgd  16457  lcmgcdlem  16493  isprm6  16601  phiprmpw  16659  pcneg  16757  prmpwdvds  16787  4sqlem19  16846  0ramcl  16906  imasleval  17437  catpropd  17603  funcres2c  17802  initoeu2  17916  latdisdlem  18399  acsfiindd  18456  dirtr  18505  mndind  18652  grpinveu  18799  mulgnn0subcl  18903  mulgsubcl  18904  mhmmulg  18931  cycsubm  19009  cycsubgcl  19013  cycsubgss  19014  ghmmulg  19034  odf1  19358  dfod2  19360  gexdvds2  19381  sylow2blem3  19418  frgpup1  19571  iscyggen2  19672  iscyg3  19677  prdsgsum  19772  ringrghm  20043  dvdsrcl2  20093  crngunit  20105  dvdsrpropd  20141  lss1d  20481  quscrng  20769  mulgghm2  20934  frgpcyg  21017  ip0r  21078  isphld  21095  frlmgsum  21215  uvcresum  21236  coe1tmmul  21685  mdetdiagid  21986  cpmatmcllem  22104  tgcl  22356  0ntr  22459  innei  22513  neitr  22568  ordtrest2lem  22591  cncnp  22668  cnnei  22670  2ndcdisj  22844  dislly  22885  dissnlocfin  22917  kgenss  22931  ptcnplem  23009  ptcnp  23010  ptcn  23015  cnmpt2k  23076  qtoprest  23105  kqt0lem  23124  isr0  23125  kqreglem1  23129  trfilss  23277  isufil2  23296  ufileu  23307  hausflim  23369  cnextcn  23455  symgtgp  23494  tsmssubm  23531  tsmsxplem1  23541  ustfilxp  23601  ustuqtop0  23629  elbl2ps  23779  elbl2  23780  nrginvrcn  24093  nmoix  24130  nmoleub  24132  cncfco  24307  icccvx  24350  iscmet3  24694  rrxmet  24809  ovolfioo  24868  ovolficc  24869  ovolicc2lem4  24921  iunmbl2  24958  dyadmax  24999  mbfsup  25065  mbflimsup  25067  mbflim  25069  itg1addlem4  25100  itg1addlem4OLD  25101  mbfi1flimlem  25124  itg2monolem1  25152  itg2mono  25155  itg2i1fseqle  25156  itg2i1fseq  25157  itg2addlem  25160  itg2gt0  25162  itg2cnlem1  25163  itgfsum  25228  cnlimc  25289  dvlip2  25396  itgsubst  25450  plyeq0lem  25608  plypf1  25610  dvtaylp  25766  ulmcaulem  25790  ulmcau  25791  ulmcn  25795  ulmdvlem3  25798  mtest  25800  pserulm  25818  pserdvlem2  25824  logdivlt  26013  advlogexp  26047  cxpexp  26060  cxpcl  26066  xrlimcnp  26355  basellem4  26470  logexprlim  26610  dchrsum2  26653  sumdchr2  26655  rpvmasum2  26897  pntrsumbnd2  26952  pntleml  26996  noreson  27045  tglineeltr  27636  brbtwn2  27917  colinearalglem4  27921  axeuclidlem  27974  axcontlem8  27983  axcontlem10  27985  grpoidinvlem3  29511  grpoideu  29514  grpoinveu  29524  nmcvcn  29700  nmounbi  29781  blocnilem  29809  ubthlem1  29875  h2hlm  29985  ocsh  30288  brafnmul  30956  kbpj  30961  nmcexi  31031  lnconi  31038  riesz1  31070  mdbr2  31301  mdsl0  31315  mdslmd3i  31337  csmdsymi  31339  atcvatlem  31390  chirredlem1  31395  chirredi  31399  cdj3lem2b  31442  xrge0infss  31733  oduprs  31894  mgcmntco  31924  lmodvslmhm  31962  submarchi  32092  grplsm0l  32257  ssmxidllem  32314  lindsunlem  32406  lindsun  32407  madjusmdetlem2  32498  zarcmplem  32551  ordtrest2NEWlem  32592  voliune  32917  fsum2dsub  33309  circlemeth  33342  bnj110  33559  cvxsconn  33924  btwnouttr2  34683  cgrxfr  34716  btwnxfr  34717  lineext  34737  segcon2  34766  brsegle2  34770  seglecgr12im  34771  segletr  34775  broutsideof3  34787  outsideofeu  34792  lineunray  34808  lineelsb2  34809  neibastop3  34910  bj-imdiridlem  35729  isbasisrelowllem1  35899  isbasisrelowllem2  35900  fvineqsneu  35955  unccur  36134  fin2solem  36137  lindsadd  36144  matunitlindflem1  36147  matunitlindflem2  36148  poimirlem4  36155  poimirlem6  36157  poimirlem7  36158  poimirlem22  36173  poimirlem23  36174  poimirlem25  36176  poimirlem26  36177  poimirlem28  36179  poimirlem30  36181  poimirlem31  36182  poimirlem32  36183  poimir  36184  broucube  36185  heicant  36186  mblfinlem3  36190  volsupnfl  36196  itg2addnclem  36202  itg2addnclem2  36203  itg2addnclem3  36204  ftc1anclem1  36224  ftc1anclem5  36228  ftc1anclem6  36229  ftc1anc  36232  unirep  36245  filbcmb  36272  fzmul  36273  fdc  36277  nninfnub  36283  isbnd2  36315  bndss  36318  prdsbnd  36325  prdstotbnd  36326  ismtyres  36340  rrnmet  36361  rrncmslem  36364  rrnequiv  36367  ghomco  36423  grpokerinj  36425  rngonegmn1l  36473  isdrngo2  36490  rngoisocnv  36513  divrngidl  36560  intidl  36561  unichnidl  36563  prnc  36599  isfldidl  36600  cvrexchlem  37955  ps-2  38014  3atnelvolN  38122  dib1dim  39701  dib1dim2  39704  pwsgprod  40790  fsuppind  40823  mzpindd  41127  dvdsabsmod0  41369  radcnvrat  42716  expgrowth  42737  fnchoice  43356  infxrbnd2  43724  infleinflem2  43726  xrralrecnnge  43745  limsuppnfdlem  44062  icccncfext  44248  dvnmul  44304  dvnprodlem2  44308  stoweidlem17  44378  stoweidlem30  44391  stoweidlem38  44399  stoweidlem42  44403  stoweidlem44  44405  fourierdlem31  44499  fourierdlem73  44540  fourierdlem74  44541  fourierdlem75  44542  fourierdlem83  44550  fourierdlem94  44561  fourierdlem113  44580  etransclem4  44599  iinhoiicclem  45034  iccvonmbllem  45039  smfsuplem1  45172  smfsupdmmbllem  45205  smfinfdmmbllem  45209  mndpsuppss  46567  itsclquadeu  46983  aacllem  47368