Theorem an32s 652

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 646	. 2 ⊢ (((𝜑 ∧ 𝜒) ∧ 𝜓) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒))
2		an32s.1	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
3	1, 2	sylbi 217	1 ⊢ (((𝜑 ∧ 𝜒) ∧ 𝜓) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  anass1rs  655  anabss1  666  biadanid  822  wereu2  5638  ordintdif  6386  ordunisssuc  6443  fssres  6729  dffv2  6959  isocnv  7308  f1oiso  7329  f1ocnvfv3  7385  fiunlem  7923  onfununi  8313  oev2  8490  oaordi  8513  oaass  8528  omlimcl  8545  odi  8546  omass  8547  oewordri  8559  oelim2  8562  oeoa  8564  oeoe  8566  nnaordi  8585  omabs  8618  eceqoveq  8798  mapxpen  9113  mapdom2  9118  findcard  9133  dif1ennnALT  9229  fimax2g  9240  isfinite2  9252  fimin2g  9457  rankval3b  9786  isf32lem9  10321  fin1a2s  10374  zornn0g  10465  gchen1  10585  gchen2  10586  intwun  10695  suplem2pr  11013  recexsrlem  11063  axpre-sup  11129  axsup  11256  dedekind  11344  recextlem2  11816  divne0  11856  dfinfre  12171  qreccl  12935  xrlttr  13107  xaddf  13191  xrsupsslem  13274  xrinfmsslem  13275  supxr2  13281  supxrunb1  13286  supxrbnd1  13288  supxrbnd2  13289  modid  13865  seqof  14031  cau3lem  15328  lo1bdd2  15497  o1co  15559  rlimcn3  15563  climcn1  15565  climcn2  15566  rlimsqzlem  15622  caucvgb  15653  fsumrlim  15784  fsumo1  15785  ntrivcvg  15870  rplpwr  16535  dvdssq  16544  nn0seqcvgd  16547  lcmgcdlem  16583  isprm6  16691  phiprmpw  16753  pcneg  16852  prmpwdvds  16882  4sqlem19  16941  0ramcl  17001  imasleval  17511  catpropd  17677  funcres2c  17872  initoeu2  17985  oduprs  18268  latdisdlem  18462  acsfiindd  18519  dirtr  18568  mndpsuppss  18699  mndind  18762  grpinveu  18913  mulgnn0subcl  19026  mulgsubcl  19027  mhmmulg  19054  cycsubm  19141  cycsubgcl  19145  cycsubgss  19146  ghmmulg  19167  odf1  19499  dfod2  19501  gexdvds2  19522  sylow2blem3  19559  frgpup1  19712  iscyggen2  19818  iscyg3  19823  prdsgsum  19918  ringrghm  20229  dvdsrcl2  20282  crngunit  20294  dvdsrpropd  20332  lss1d  20876  quscrng  21200  mulgghm2  21393  frgpcyg  21490  ip0r  21553  isphld  21570  frlmgsum  21688  uvcresum  21709  psdmul  22060  coe1tmmul  22170  mdetdiagid  22494  cpmatmcllem  22612  tgcl  22863  0ntr  22965  innei  23019  neitr  23074  ordtrest2lem  23097  cncnp  23174  cnnei  23176  2ndcdisj  23350  dislly  23391  dissnlocfin  23423  kgenss  23437  ptcnplem  23515  ptcnp  23516  ptcn  23521  cnmpt2k  23582  qtoprest  23611  kqt0lem  23630  isr0  23631  kqreglem1  23635  trfilss  23783  isufil2  23802  ufileu  23813  hausflim  23875  cnextcn  23961  symgtgp  24000  tsmssubm  24037  tsmsxplem1  24047  ustfilxp  24107  ustuqtop0  24135  elbl2ps  24284  elbl2  24285  nrginvrcn  24587  nmoix  24624  nmoleub  24626  cncfco  24807  icccvx  24855  iscmet3  25200  rrxmet  25315  ovolfioo  25375  ovolficc  25376  ovolicc2lem4  25428  iunmbl2  25465  dyadmax  25506  mbfsup  25572  mbflimsup  25574  mbflim  25576  itg1addlem4  25607  mbfi1flimlem  25630  itg2monolem1  25658  itg2mono  25661  itg2i1fseqle  25662  itg2i1fseq  25663  itg2addlem  25666  itg2gt0  25668  itg2cnlem1  25669  itgfsum  25735  cnlimc  25796  dvlip2  25907  itgsubst  25963  plyeq0lem  26122  plypf1  26124  dvtaylp  26285  ulmcaulem  26310  ulmcau  26311  ulmcn  26315  ulmdvlem3  26318  mtest  26320  pserulm  26338  pserdvlem2  26345  logdivlt  26537  advlogexp  26571  cxpexp  26584  cxpcl  26590  xrlimcnp  26885  basellem4  27001  logexprlim  27143  dchrsum2  27186  sumdchr2  27188  rpvmasum2  27430  pntrsumbnd2  27485  pntleml  27529  noreson  27579  tglineeltr  28565  brbtwn2  28839  colinearalglem4  28843  axeuclidlem  28896  axcontlem8  28905  axcontlem10  28907  grpoidinvlem3  30442  grpoideu  30445  grpoinveu  30455  nmcvcn  30631  nmounbi  30712  blocnilem  30740  ubthlem1  30806  h2hlm  30916  ocsh  31219  brafnmul  31887  kbpj  31892  nmcexi  31962  lnconi  31969  riesz1  32001  mdbr2  32232  mdsl0  32246  mdslmd3i  32268  csmdsymi  32270  atcvatlem  32321  chirredlem1  32326  chirredi  32330  cdj3lem2b  32373  xrge0infss  32690  mgcmntco  32927  chnind  32944  lmodvslmhm  32997  gsumwrd2dccatlem  33013  submarchi  33147  dvdsruasso  33363  grplsm0l  33381  ssdifidllem  33434  ssdifidlprm  33436  ssmxidllem  33451  rprmndvdsru  33507  r1plmhm  33582  lindsunlem  33627  lindsun  33628  fldextrspunlsplem  33675  madjusmdetlem2  33825  zarcmplem  33878  ordtrest2NEWlem  33919  voliune  34226  fsum2dsub  34605  circlemeth  34638  bnj110  34855  cvxsconn  35237  btwnouttr2  36017  cgrxfr  36050  btwnxfr  36051  lineext  36071  segcon2  36100  brsegle2  36104  seglecgr12im  36105  segletr  36109  broutsideof3  36121  outsideofeu  36126  lineunray  36142  lineelsb2  36143  neibastop3  36357  bj-imdiridlem  37180  isbasisrelowllem1  37350  isbasisrelowllem2  37351  fvineqsneu  37406  unccur  37604  fin2solem  37607  lindsadd  37614  matunitlindflem1  37617  matunitlindflem2  37618  poimirlem4  37625  poimirlem6  37627  poimirlem7  37628  poimirlem22  37643  poimirlem23  37644  poimirlem25  37646  poimirlem26  37647  poimirlem28  37649  poimirlem30  37651  poimirlem31  37652  poimirlem32  37653  poimir  37654  broucube  37655  heicant  37656  mblfinlem3  37660  volsupnfl  37666  itg2addnclem  37672  itg2addnclem2  37673  itg2addnclem3  37674  ftc1anclem1  37694  ftc1anclem5  37698  ftc1anclem6  37699  ftc1anc  37702  unirep  37715  filbcmb  37741  fzmul  37742  fdc  37746  nninfnub  37752  isbnd2  37784  bndss  37787  prdsbnd  37794  prdstotbnd  37795  ismtyres  37809  rrnmet  37830  rrncmslem  37833  rrnequiv  37836  ghomco  37892  grpokerinj  37894  rngonegmn1l  37942  isdrngo2  37959  rngoisocnv  37982  divrngidl  38029  intidl  38030  unichnidl  38032  prnc  38068  isfldidl  38069  cvrexchlem  39420  ps-2  39479  3atnelvolN  39587  dib1dim  41166  dib1dim2  41169  f1o2d2  42228  expeqidd  42320  pwsgprod  42539  evlselv  42582  fsuppind  42585  mzpindd  42741  dvdsabsmod0  42983  radcnvrat  44310  expgrowth  44331  modelac8prim  44989  fnchoice  45030  infxrbnd2  45372  infleinflem2  45374  xrralrecnnge  45393  limsuppnfdlem  45706  icccncfext  45892  dvnmul  45948  dvnprodlem2  45952  stoweidlem17  46022  stoweidlem30  46035  stoweidlem38  46043  stoweidlem42  46047  stoweidlem44  46049  fourierdlem31  46143  fourierdlem73  46184  fourierdlem74  46185  fourierdlem75  46186  fourierdlem83  46194  fourierdlem94  46205  fourierdlem113  46224  etransclem4  46243  iinhoiicclem  46678  iccvonmbllem  46683  smfsuplem1  46816  smfsupdmmbllem  46849  smfinfdmmbllem  46853  itsclquadeu  48770  aacllem  49794