Theorem an32s 665

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  anass1rs  668  anabss1  679  biadanid  835  wereu2  5655  ordintdif  6440  ordunisssuc  6497  fssres  6778  dffv2  7011  isocnv  7369  f1oiso  7390  f1ocnvfv3  7446  fiunlem  7988  mpof1o2d  8174  onfununi  8387  oev2  8569  oaordi  8592  oaass  8607  omlimcl  8624  odi  8625  omass  8626  oewordri  8639  oelim2  8642  oeoa  8644  oeoe  8646  nnaordi  8665  omabs  8698  eceqoveq  8881  mapxpen  9200  mapdom2  9205  findcard  9217  dif1ennnALT  9306  fimax2g  9315  isfinite2  9328  fimin2g  9528  rankval3b  9873  isf32lem9  10478  fin1a2s  10531  zornn0g  10622  gchen1  10749  gchen2  10750  intwun  10859  suplem2pr  11177  recexsrlem  11227  axpre-sup  11293  axsup  11424  dedekind  11512  recextlem2  11987  divne0  12026  dfinfre  12338  qreccl  13137  xrlttr  13309  xaddf  13394  xrsupsslem  13477  xrinfmsslem  13478  supxr2  13484  supxrunb1  13489  supxrbnd1  13491  supxrbnd2  13492  modid  14076  seqof  14242  cau3lem  15566  lo1bdd2  15735  o1co  15797  rlimcn3  15801  climcn1  15803  climcn2  15804  rlimsqzlem  15860  caucvgb  15891  fsumrlim  16022  fsumo1  16023  ntrivcvg  16110  rplpwr  16776  dvdssq  16786  nn0seqcvgd  16789  lcmgcdlem  16825  isprm6  16934  phiprmpw  16997  pcneg  17096  prmpwdvds  17126  4sqlem19  17185  0ramcl  17245  imasleval  17763  catpropd  17933  funcres2c  18128  initoeu2  18241  oduprs  18524  latdisdlem  18720  acsfiindd  18777  dirtr  18826  chnind  18845  mndpsuppss  19009  mndind  19074  grpinveu  19235  mulgnn0subcl  19347  mulgsubcl  19348  mhmmulg  19375  cycsubm  19467  cycsubgcl  19471  cycsubgss  19472  ghmmulg  19492  odf1  19827  dfod2  19829  gexdvds2  19850  sylow2blem3  19887  frgpup1  20040  iscyggen2  20146  iscyg3  20151  prdsgsum  20246  ringrghm  20595  pwsgprod  20610  dvdsrcl2  20647  crngunit  20659  dvdsrpropd  20697  isdrng3lem2  21057  lss1d  21289  quscrng  21630  ssdifidllem  21691  ssdifidlprm  21693  mulgghm2  21837  frgpcyg  21934  ip0r  21998  isphld  22015  frlmgsum  22133  uvcresum  22154  psdmul  22542  coe1tmmul  22651  mdetdiagid  22970  matunitlindflem1  23049  matunitlindflem2  23050  cpmatmcllem  23091  tgcl  23342  0ntr  23444  innei  23498  neitr  23553  ordtrest2lem  23576  cncnp  23653  cnnei  23655  2ndcdisj  23830  dislly  23871  dissnlocfin  23903  kgenss  23917  ptcnplem  23995  ptcnp  23996  ptcn  24001  cnmpt2k  24062  qtoprest  24091  kqt0lem  24110  isr0  24111  kqreglem1  24115  trfilss  24263  isufil2  24282  ufileu  24293  hausflim  24355  cnextcn  24441  symgtgp  24480  tsmssubm  24517  tsmsxplem1  24527  ustfilxp  24587  ustuqtop0  24614  elbl2ps  24763  elbl2  24764  nrginvrcn  25066  nmoix  25103  nmoleub  25105  cncfco  25283  icccvx  25326  iscmet3  25669  rrxmet  25784  ovolfioo  25843  ovolficc  25844  ovolicc2lem4  25896  iunmbl2  25933  dyadmax  25974  mbfsup  26040  mbflimsup  26042  mbflim  26044  itg1addlem4  26075  mbfi1flimlem  26098  itg2monolem1  26126  itg2mono  26129  itg2i1fseqle  26130  itg2i1fseq  26131  itg2addlem  26134  itg2gt0  26136  itg2cnlem1  26137  itgfsum  26202  cnlimc  26263  dvlip2  26370  itgsubst  26424  plyeq0lem  26584  plypf1  26586  dvtaylp  26754  ulmcaulem  26778  ulmcau  26779  ulmcn  26783  ulmdvlem3  26786  mtest  26788  pserulm  26806  pserdvlem2  26812  logdivlt  27006  advlogexp  27040  cxpexp  27053  cxpcl  27059  xrlimcnp  27353  basellem4  27468  logexprlim  27609  dchrsum2  27652  sumdchr2  27654  rpvmasum2  27896  pntrsumbnd2  27951  pntleml  27995  noreson  28074  z12zsodd  28925  tglineeltr  29156  plngrotlem2  29323  brbtwn2  29540  colinearalglem4  29544  axeuclidlem  29597  axcontlem8  29606  axcontlem10  29608  grpoidinvlem3  31165  grpoideu  31168  grpoinveu  31178  nmcvcn  31354  nmounbi  31435  blocnilem  31463  ubthlem1  31529  h2hlm  31639  ocsh  31942  brafnmul  32610  kbpj  32615  nmcexi  32685  lnconi  32692  riesz1  32724  mdbr2  32955  mdsl0  32969  mdslmd3i  32991  csmdsymi  32993  atcvatlem  33044  chirredlem1  33049  chirredi  33053  cdj3lem2b  33096  xrge0infss  33448  mgcmntco  33654  lmodvslmhm  33710  suppgsumssiun  33732  gsumwrd2dccatlem  33737  submarchi  33846  dvdsruasso  34044  grplsm0l  34058  ssmxidllem  34102  rprmndvdsru  34165  r1plmhm  34246  mplvrpmmhm  34289  mplvrpmrhm  34290  esplyfval1  34316  lindsunlem  34367  lindsun  34368  fldextrspunlsplem  34416  extdgfialglem2  34436  madjusmdetlem2  34571  zarcmplem  34624  ordtrest2NEWlem  34665  voliune  34973  fsum2dsub  35347  circlemeth  35380  bnj110  35599  cvxsconn  36216  btwnouttr2  37002  cgrxfr  37035  btwnxfr  37036  lineext  37056  segcon2  37085  brsegle2  37089  seglecgr12im  37090  segletr  37094  broutsideof3  37106  outsideofeu  37111  lineunray  37127  lineelsb2  37128  nmulrid  37161  neibastop3  37365  ttcmin  37499  bj-imdiridlem  38374  isbasisrelowllem1  38546  isbasisrelowllem2  38547  fvineqsneu  38602  unccur  38794  fin2solem  38797  lindsadd  38804  poimirlem4  38810  poimirlem6  38812  poimirlem7  38813  poimirlem22  38828  poimirlem23  38829  poimirlem25  38831  poimirlem26  38832  poimirlem28  38834  poimirlem30  38836  poimirlem31  38837  poimirlem32  38838  poimir  38839  broucube  38840  heicant  38841  mblfinlem3  38845  volsupnfl  38851  itg2addnclem  38857  itg2addnclem2  38858  itg2addnclem3  38859  ftc1anclem1  38879  ftc1anclem5  38883  ftc1anclem6  38884  ftc1anc  38887  unirep  38916  filbcmb  38940  fzmul  38941  fdc  38945  nninfnub  38951  isbnd2  38983  bndss  38986  prdsbnd  38993  prdstotbnd  38994  ismtyres  39008  rrnmet  39029  rrncmslem  39032  rrnequiv  39035  ghomco  39091  grpokerinj  39093  rngonegmn1l  39141  isdrngo2  39158  rngoisocnv  39181  divrngidl  39228  intidl  39229  unichnidl  39231  prnc  39267  isfldidl  39268  cvrexchlem  40742  ps-2  40801  3atnelvolN  40909  dib1dim  42488  dib1dim2  42491  expeqidd  43648  evlselv  43883  fsuppind  43884  mzpindd  44023  dvdsabsmod0  44260  radcnvrat  45559  expgrowth  45580  modelac8prim  46246  fnchoice  46320  infxrbnd2  46653  infleinflem2  46655  xrralrecnnge  46674  limsuppnfdlem  46984  icccncfext  47170  dvnmul  47226  dvnprodlem2  47230  stoweidlem17  47300  stoweidlem30  47313  stoweidlem38  47321  stoweidlem42  47325  stoweidlem44  47327  fourierdlem31  47421  fourierdlem73  47462  fourierdlem74  47463  fourierdlem75  47464  fourierdlem83  47472  fourierdlem94  47483  fourierdlem113  47502  etransclem4  47521  hoicvr  47831  iinhoiicclem  47956  iccvonmbllem  47961  smfsuplem1  48094  smfsupdmmbllem  48127  smfinfdmmbllem  48131  itsclquadeu  50220  aacllem  51367  veroquadmodzerod  51412