Theorem an32s 658

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 652	. 2 ⊢ (((𝜑 ∧ 𝜒) ∧ 𝜓) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒))
2		an32s.1	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
3	1, 2	sylbi 218	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 208  df-an 397

This theorem is referenced by:  anass1rs  661  anabss1  672  biadanid  828  wereu2  5615  ordintdif  6361  ordunisssuc  6418  fssres  6693  dffv2  6922  isocnv  7274  f1oiso  7295  f1ocnvfv3  7351  fiunlem  7884  mpof1o2d  8065  onfununi  8271  oev2  8448  oaordi  8471  oaass  8486  omlimcl  8503  odi  8504  omass  8505  oewordri  8518  oelim2  8521  oeoa  8523  oeoe  8525  nnaordi  8544  omabs  8577  eceqoveq  8759  mapxpen  9071  mapdom2  9076  findcard  9088  dif1ennnALT  9177  fimax2g  9186  isfinite2  9198  fimin2g  9402  rankval3b  9741  isf32lem9  10274  fin1a2s  10327  zornn0g  10418  gchen1  10539  gchen2  10540  intwun  10649  suplem2pr  10967  recexsrlem  11017  axpre-sup  11083  axsup  11212  dedekind  11300  recextlem2  11772  divne0  11812  dfinfre  12128  qreccl  12910  xrlttr  13082  xaddf  13167  xrsupsslem  13250  xrinfmsslem  13251  supxr2  13257  supxrunb1  13262  supxrbnd1  13264  supxrbnd2  13265  modid  13846  seqof  14012  cau3lem  15308  lo1bdd2  15477  o1co  15539  rlimcn3  15543  climcn1  15545  climcn2  15546  rlimsqzlem  15602  caucvgb  15633  fsumrlim  15765  fsumo1  15766  ntrivcvg  15853  rplpwr  16518  dvdssq  16527  nn0seqcvgd  16530  lcmgcdlem  16566  isprm6  16675  phiprmpw  16737  pcneg  16836  prmpwdvds  16866  4sqlem19  16925  0ramcl  16985  imasleval  17496  catpropd  17666  funcres2c  17861  initoeu2  17974  oduprs  18257  latdisdlem  18453  acsfiindd  18510  dirtr  18559  chnind  18578  mndpsuppss  18724  mndind  18787  grpinveu  18941  mulgnn0subcl  19054  mulgsubcl  19055  mhmmulg  19082  cycsubm  19168  cycsubgcl  19172  cycsubgss  19173  ghmmulg  19194  odf1  19528  dfod2  19530  gexdvds2  19551  sylow2blem3  19588  frgpup1  19741  iscyggen2  19847  iscyg3  19852  prdsgsum  19947  ringrghm  20285  pwsgprod  20300  dvdsrcl2  20337  crngunit  20349  dvdsrpropd  20387  lss1d  20953  quscrng  21276  mulgghm2  21451  frgpcyg  21548  ip0r  21612  isphld  21629  frlmgsum  21747  uvcresum  21768  psdmul  22154  coe1tmmul  22263  mdetdiagid  22583  cpmatmcllem  22701  tgcl  22952  0ntr  23054  innei  23108  neitr  23163  ordtrest2lem  23186  cncnp  23263  cnnei  23265  2ndcdisj  23439  dislly  23480  dissnlocfin  23512  kgenss  23526  ptcnplem  23604  ptcnp  23605  ptcn  23610  cnmpt2k  23671  qtoprest  23700  kqt0lem  23719  isr0  23720  kqreglem1  23724  trfilss  23872  isufil2  23891  ufileu  23902  hausflim  23964  cnextcn  24050  symgtgp  24089  tsmssubm  24126  tsmsxplem1  24136  ustfilxp  24196  ustuqtop0  24223  elbl2ps  24372  elbl2  24373  nrginvrcn  24675  nmoix  24712  nmoleub  24714  cncfco  24892  icccvx  24935  iscmet3  25278  rrxmet  25393  ovolfioo  25452  ovolficc  25453  ovolicc2lem4  25505  iunmbl2  25542  dyadmax  25583  mbfsup  25649  mbflimsup  25651  mbflim  25653  itg1addlem4  25684  mbfi1flimlem  25707  itg2monolem1  25735  itg2mono  25738  itg2i1fseqle  25739  itg2i1fseq  25740  itg2addlem  25743  itg2gt0  25745  itg2cnlem1  25746  itgfsum  25812  cnlimc  25873  dvlip2  25980  itgsubst  26034  plyeq0lem  26193  plypf1  26195  dvtaylp  26353  ulmcaulem  26377  ulmcau  26378  ulmcn  26382  ulmdvlem3  26385  mtest  26387  pserulm  26405  pserdvlem2  26411  logdivlt  26603  advlogexp  26637  cxpexp  26650  cxpcl  26656  xrlimcnp  26950  basellem4  27065  logexprlim  27206  dchrsum2  27249  sumdchr2  27251  rpvmasum2  27493  pntrsumbnd2  27548  pntleml  27592  noreson  27642  z12zsodd  28492  tglineeltr  28717  brbtwn2  28992  colinearalglem4  28996  axeuclidlem  29049  axcontlem8  29058  axcontlem10  29060  grpoidinvlem3  30595  grpoideu  30598  grpoinveu  30608  nmcvcn  30784  nmounbi  30865  blocnilem  30893  ubthlem1  30959  h2hlm  31069  ocsh  31372  brafnmul  32040  kbpj  32045  nmcexi  32115  lnconi  32122  riesz1  32154  mdbr2  32385  mdsl0  32399  mdslmd3i  32421  csmdsymi  32423  atcvatlem  32474  chirredlem1  32479  chirredi  32483  cdj3lem2b  32526  xrge0infss  32852  mgcmntco  33073  lmodvslmhm  33131  suppgsumssiun  33153  gsumwrd2dccatlem  33158  submarchi  33267  dvdsruasso  33468  grplsm0l  33486  ssdifidllem  33539  ssdifidlprm  33541  ssmxidllem  33556  rprmndvdsru  33612  r1plmhm  33693  mplvrpmmhm  33730  mplvrpmrhm  33731  esplyfval1  33757  lindsunlem  33808  lindsun  33809  fldextrspunlsplem  33857  extdgfialglem2  33877  madjusmdetlem2  34012  zarcmplem  34065  ordtrest2NEWlem  34106  voliune  34413  fsum2dsub  34791  circlemeth  34824  bnj110  35040  cvxsconn  35471  btwnouttr2  36250  cgrxfr  36283  btwnxfr  36284  lineext  36304  segcon2  36333  brsegle2  36337  seglecgr12im  36338  segletr  36342  broutsideof3  36354  outsideofeu  36359  lineunray  36375  lineelsb2  36376  neibastop3  36590  ttcmin  36724  mh-inf3f1  36769  bj-imdiridlem  37545  isbasisrelowllem1  37717  isbasisrelowllem2  37718  fvineqsneu  37773  unccur  37970  fin2solem  37973  lindsadd  37980  matunitlindflem1  37983  matunitlindflem2  37984  poimirlem4  37991  poimirlem6  37993  poimirlem7  37994  poimirlem22  38009  poimirlem23  38010  poimirlem25  38012  poimirlem26  38013  poimirlem28  38015  poimirlem30  38017  poimirlem31  38018  poimirlem32  38019  poimir  38020  broucube  38021  heicant  38022  mblfinlem3  38026  volsupnfl  38032  itg2addnclem  38038  itg2addnclem2  38039  itg2addnclem3  38040  ftc1anclem1  38060  ftc1anclem5  38064  ftc1anclem6  38065  ftc1anc  38068  unirep  38081  filbcmb  38107  fzmul  38108  fdc  38112  nninfnub  38118  isbnd2  38150  bndss  38153  prdsbnd  38160  prdstotbnd  38161  ismtyres  38175  rrnmet  38196  rrncmslem  38199  rrnequiv  38202  ghomco  38258  grpokerinj  38260  rngonegmn1l  38308  isdrngo2  38325  rngoisocnv  38348  divrngidl  38395  intidl  38396  unichnidl  38398  prnc  38434  isfldidl  38435  cvrexchlem  39911  ps-2  39970  3atnelvolN  40078  dib1dim  41657  dib1dim2  41660  expeqidd  42802  evlselv  43039  fsuppind  43040  mzpindd  43195  dvdsabsmod0  43432  radcnvrat  44758  expgrowth  44779  modelac8prim  45436  fnchoice  45477  infxrbnd2  45813  infleinflem2  45815  xrralrecnnge  45834  limsuppnfdlem  46144  icccncfext  46330  dvnmul  46386  dvnprodlem2  46390  stoweidlem17  46460  stoweidlem30  46473  stoweidlem38  46481  stoweidlem42  46485  stoweidlem44  46487  fourierdlem31  46581  fourierdlem73  46622  fourierdlem74  46623  fourierdlem75  46624  fourierdlem83  46632  fourierdlem94  46643  fourierdlem113  46662  etransclem4  46681  hoicvr  46991  iinhoiicclem  47116  iccvonmbllem  47121  smfsuplem1  47254  smfsupdmmbllem  47287  smfinfdmmbllem  47291  itsclquadeu  49268  aacllem  50291