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

Syntax hints:   → wi 4   ∧ wa 397

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 398

This theorem is referenced by:  anass1rs  654  anabss1  665  biadanid  822  wereu2  5674  ordintdif  6415  ordunisssuc  6471  fssres  6758  dffv2  6987  isocnv  7327  f1oiso  7348  f1ocnvfv3  7404  fiunlem  7928  onfununi  8341  oev2  8523  oaordi  8546  oaass  8561  omlimcl  8578  odi  8579  omass  8580  oewordri  8592  oelim2  8595  oeoa  8597  oeoe  8599  nnaordi  8618  omabs  8650  eceqoveq  8816  mapxpen  9143  mapdom2  9148  findcard  9163  dif1ennnALT  9277  fimax2g  9289  isfinite2  9301  fimin2g  9492  rankval3b  9821  isf32lem9  10356  fin1a2s  10409  zornn0g  10500  gchen1  10620  gchen2  10621  intwun  10730  suplem2pr  11048  recexsrlem  11098  axpre-sup  11164  axsup  11289  dedekind  11377  recextlem2  11845  divne0  11884  dfinfre  12195  qreccl  12953  xrlttr  13119  xaddf  13203  xrsupsslem  13286  xrinfmsslem  13287  supxr2  13293  supxrunb1  13298  supxrbnd1  13300  supxrbnd2  13301  modid  13861  seqof  14025  cau3lem  15301  lo1bdd2  15468  o1co  15530  rlimcn3  15534  climcn1  15536  climcn2  15537  rlimsqzlem  15595  caucvgb  15626  fsumrlim  15757  fsumo1  15758  ntrivcvg  15843  rplpwr  16499  dvdssq  16504  nn0seqcvgd  16507  lcmgcdlem  16543  isprm6  16651  phiprmpw  16709  pcneg  16807  prmpwdvds  16837  4sqlem19  16896  0ramcl  16956  imasleval  17487  catpropd  17653  funcres2c  17852  initoeu2  17966  latdisdlem  18449  acsfiindd  18506  dirtr  18555  mndind  18709  grpinveu  18859  mulgnn0subcl  18967  mulgsubcl  18968  mhmmulg  18995  cycsubm  19079  cycsubgcl  19083  cycsubgss  19084  ghmmulg  19104  odf1  19430  dfod2  19432  gexdvds2  19453  sylow2blem3  19490  frgpup1  19643  iscyggen2  19749  iscyg3  19754  prdsgsum  19849  ringrghm  20125  dvdsrcl2  20180  crngunit  20192  dvdsrpropd  20230  lss1d  20574  quscrng  20878  mulgghm2  21046  frgpcyg  21129  ip0r  21190  isphld  21207  frlmgsum  21327  uvcresum  21348  coe1tmmul  21799  mdetdiagid  22102  cpmatmcllem  22220  tgcl  22472  0ntr  22575  innei  22629  neitr  22684  ordtrest2lem  22707  cncnp  22784  cnnei  22786  2ndcdisj  22960  dislly  23001  dissnlocfin  23033  kgenss  23047  ptcnplem  23125  ptcnp  23126  ptcn  23131  cnmpt2k  23192  qtoprest  23221  kqt0lem  23240  isr0  23241  kqreglem1  23245  trfilss  23393  isufil2  23412  ufileu  23423  hausflim  23485  cnextcn  23571  symgtgp  23610  tsmssubm  23647  tsmsxplem1  23657  ustfilxp  23717  ustuqtop0  23745  elbl2ps  23895  elbl2  23896  nrginvrcn  24209  nmoix  24246  nmoleub  24248  cncfco  24423  icccvx  24466  iscmet3  24810  rrxmet  24925  ovolfioo  24984  ovolficc  24985  ovolicc2lem4  25037  iunmbl2  25074  dyadmax  25115  mbfsup  25181  mbflimsup  25183  mbflim  25185  itg1addlem4  25216  itg1addlem4OLD  25217  mbfi1flimlem  25240  itg2monolem1  25268  itg2mono  25271  itg2i1fseqle  25272  itg2i1fseq  25273  itg2addlem  25276  itg2gt0  25278  itg2cnlem1  25279  itgfsum  25344  cnlimc  25405  dvlip2  25512  itgsubst  25566  plyeq0lem  25724  plypf1  25726  dvtaylp  25882  ulmcaulem  25906  ulmcau  25907  ulmcn  25911  ulmdvlem3  25914  mtest  25916  pserulm  25934  pserdvlem2  25940  logdivlt  26129  advlogexp  26163  cxpexp  26176  cxpcl  26182  xrlimcnp  26473  basellem4  26588  logexprlim  26728  dchrsum2  26771  sumdchr2  26773  rpvmasum2  27015  pntrsumbnd2  27070  pntleml  27114  noreson  27163  tglineeltr  27882  brbtwn2  28163  colinearalglem4  28167  axeuclidlem  28220  axcontlem8  28229  axcontlem10  28231  grpoidinvlem3  29759  grpoideu  29762  grpoinveu  29772  nmcvcn  29948  nmounbi  30029  blocnilem  30057  ubthlem1  30123  h2hlm  30233  ocsh  30536  brafnmul  31204  kbpj  31209  nmcexi  31279  lnconi  31286  riesz1  31318  mdbr2  31549  mdsl0  31563  mdslmd3i  31585  csmdsymi  31587  atcvatlem  31638  chirredlem1  31643  chirredi  31647  cdj3lem2b  31690  xrge0infss  31973  oduprs  32134  mgcmntco  32164  lmodvslmhm  32202  submarchi  32332  dvdsruasso  32490  grplsm0l  32513  ssmxidllem  32589  lindsunlem  32709  lindsun  32710  madjusmdetlem2  32808  zarcmplem  32861  ordtrest2NEWlem  32902  voliune  33227  fsum2dsub  33619  circlemeth  33652  bnj110  33869  cvxsconn  34234  btwnouttr2  34994  cgrxfr  35027  btwnxfr  35028  lineext  35048  segcon2  35077  brsegle2  35081  seglecgr12im  35082  segletr  35086  broutsideof3  35098  outsideofeu  35103  lineunray  35119  lineelsb2  35120  neibastop3  35247  bj-imdiridlem  36066  isbasisrelowllem1  36236  isbasisrelowllem2  36237  fvineqsneu  36292  unccur  36471  fin2solem  36474  lindsadd  36481  matunitlindflem1  36484  matunitlindflem2  36485  poimirlem4  36492  poimirlem6  36494  poimirlem7  36495  poimirlem22  36510  poimirlem23  36511  poimirlem25  36513  poimirlem26  36514  poimirlem28  36516  poimirlem30  36518  poimirlem31  36519  poimirlem32  36520  poimir  36521  broucube  36522  heicant  36523  mblfinlem3  36527  volsupnfl  36533  itg2addnclem  36539  itg2addnclem2  36540  itg2addnclem3  36541  ftc1anclem1  36561  ftc1anclem5  36565  ftc1anclem6  36566  ftc1anc  36569  unirep  36582  filbcmb  36608  fzmul  36609  fdc  36613  nninfnub  36619  isbnd2  36651  bndss  36654  prdsbnd  36661  prdstotbnd  36662  ismtyres  36676  rrnmet  36697  rrncmslem  36700  rrnequiv  36703  ghomco  36759  grpokerinj  36761  rngonegmn1l  36809  isdrngo2  36826  rngoisocnv  36849  divrngidl  36896  intidl  36897  unichnidl  36899  prnc  36935  isfldidl  36936  cvrexchlem  38290  ps-2  38349  3atnelvolN  38457  dib1dim  40036  dib1dim2  40039  f1o2d2  41055  pwsgprod  41114  evlselv  41159  fsuppind  41162  mzpindd  41484  dvdsabsmod0  41726  radcnvrat  43073  expgrowth  43094  fnchoice  43713  infxrbnd2  44079  infleinflem2  44081  xrralrecnnge  44100  limsuppnfdlem  44417  icccncfext  44603  dvnmul  44659  dvnprodlem2  44663  stoweidlem17  44733  stoweidlem30  44746  stoweidlem38  44754  stoweidlem42  44758  stoweidlem44  44760  fourierdlem31  44854  fourierdlem73  44895  fourierdlem74  44896  fourierdlem75  44897  fourierdlem83  44905  fourierdlem94  44916  fourierdlem113  44935  etransclem4  44954  iinhoiicclem  45389  iccvonmbllem  45394  smfsuplem1  45527  smfsupdmmbllem  45560  smfinfdmmbllem  45564  mndpsuppss  47047  itsclquadeu  47463  aacllem  47848