Theorem an32s 664

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

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  anass1rs  667  anabss1  678  biadanid  834  wereu2  5656  ordintdif  6410  ordunisssuc  6467  fssres  6742  dffv2  6974  isocnv  7326  f1oiso  7347  f1ocnvfv3  7403  fiunlem  7935  mpof1o2d  8117  onfununi  8324  oev2  8504  oaordi  8527  oaass  8542  omlimcl  8559  odi  8560  omass  8561  oewordri  8574  oelim2  8577  oeoa  8579  oeoe  8581  nnaordi  8600  omabs  8633  eceqoveq  8816  mapxpen  9127  mapdom2  9132  findcard  9144  dif1ennnALT  9233  fimax2g  9242  isfinite2  9254  fimin2g  9455  rankval3b  9794  isf32lem9  10341  fin1a2s  10394  zornn0g  10485  gchen1  10606  gchen2  10607  intwun  10716  suplem2pr  11034  recexsrlem  11084  axpre-sup  11150  axsup  11281  dedekind  11369  recextlem2  11841  divne0  11880  dfinfre  12192  qreccl  12989  xrlttr  13161  xaddf  13246  xrsupsslem  13329  xrinfmsslem  13330  supxr2  13336  supxrunb1  13341  supxrbnd1  13343  supxrbnd2  13344  modid  13925  seqof  14091  cau3lem  15402  lo1bdd2  15571  o1co  15633  rlimcn3  15637  climcn1  15639  climcn2  15640  rlimsqzlem  15696  caucvgb  15727  fsumrlim  15859  fsumo1  15860  ntrivcvg  15947  rplpwr  16612  dvdssq  16621  nn0seqcvgd  16624  lcmgcdlem  16660  isprm6  16769  phiprmpw  16831  pcneg  16930  prmpwdvds  16960  4sqlem19  17019  0ramcl  17079  imasleval  17591  catpropd  17761  funcres2c  17956  initoeu2  18069  oduprs  18352  latdisdlem  18548  acsfiindd  18605  dirtr  18654  chnind  18673  mndpsuppss  18819  mndind  18883  grpinveu  19037  mulgnn0subcl  19149  mulgsubcl  19150  mhmmulg  19177  cycsubm  19269  cycsubgcl  19273  cycsubgss  19274  ghmmulg  19294  odf1  19628  dfod2  19630  gexdvds2  19651  sylow2blem3  19688  frgpup1  19841  iscyggen2  19947  iscyg3  19952  prdsgsum  20047  ringrghm  20392  pwsgprod  20407  dvdsrcl2  20444  crngunit  20456  dvdsrpropd  20494  lss1d  21058  quscrng  21390  ssdifidllem  21449  ssdifidlprm  21451  mulgghm2  21591  frgpcyg  21688  ip0r  21752  isphld  21769  frlmgsum  21887  uvcresum  21908  psdmul  22294  coe1tmmul  22403  mdetdiagid  22722  cpmatmcllem  22840  tgcl  23091  0ntr  23193  innei  23247  neitr  23302  ordtrest2lem  23325  cncnp  23402  cnnei  23404  2ndcdisj  23578  dislly  23619  dissnlocfin  23651  kgenss  23665  ptcnplem  23743  ptcnp  23744  ptcn  23749  cnmpt2k  23810  qtoprest  23839  kqt0lem  23858  isr0  23859  kqreglem1  23863  trfilss  24011  isufil2  24030  ufileu  24041  hausflim  24103  cnextcn  24189  symgtgp  24228  tsmssubm  24265  tsmsxplem1  24275  ustfilxp  24335  ustuqtop0  24362  elbl2ps  24511  elbl2  24512  nrginvrcn  24814  nmoix  24851  nmoleub  24853  cncfco  25031  icccvx  25074  iscmet3  25417  rrxmet  25532  ovolfioo  25591  ovolficc  25592  ovolicc2lem4  25644  iunmbl2  25681  dyadmax  25722  mbfsup  25788  mbflimsup  25790  mbflim  25792  itg1addlem4  25823  mbfi1flimlem  25846  itg2monolem1  25874  itg2mono  25877  itg2i1fseqle  25878  itg2i1fseq  25879  itg2addlem  25882  itg2gt0  25884  itg2cnlem1  25885  itgfsum  25951  cnlimc  26012  dvlip2  26119  itgsubst  26173  plyeq0lem  26332  plypf1  26334  dvtaylp  26495  ulmcaulem  26519  ulmcau  26520  ulmcn  26524  ulmdvlem3  26527  mtest  26529  pserulm  26547  pserdvlem2  26553  logdivlt  26748  advlogexp  26782  cxpexp  26795  cxpcl  26801  xrlimcnp  27095  basellem4  27210  logexprlim  27351  dchrsum2  27394  sumdchr2  27396  rpvmasum2  27638  pntrsumbnd2  27693  pntleml  27737  noreson  27786  z12zsodd  28637  tglineeltr  28862  plngrotlem2  29024  brbtwn2  29192  colinearalglem4  29196  axeuclidlem  29249  axcontlem8  29258  axcontlem10  29260  grpoidinvlem3  30795  grpoideu  30798  grpoinveu  30808  nmcvcn  30984  nmounbi  31065  blocnilem  31093  ubthlem1  31159  h2hlm  31269  ocsh  31572  brafnmul  32240  kbpj  32245  nmcexi  32315  lnconi  32322  riesz1  32354  mdbr2  32585  mdsl0  32599  mdslmd3i  32621  csmdsymi  32623  atcvatlem  32674  chirredlem1  32679  chirredi  32683  cdj3lem2b  32726  xrge0infss  33042  mgcmntco  33251  lmodvslmhm  33307  suppgsumssiun  33329  gsumwrd2dccatlem  33334  submarchi  33443  dvdsruasso  33638  grplsm0l  33652  ssmxidllem  33697  rprmndvdsru  33760  r1plmhm  33840  mplvrpmmhm  33877  mplvrpmrhm  33878  esplyfval1  33904  lindsunlem  33955  lindsun  33956  fldextrspunlsplem  34004  extdgfialglem2  34024  madjusmdetlem2  34159  zarcmplem  34212  ordtrest2NEWlem  34253  voliune  34560  fsum2dsub  34935  circlemeth  34968  bnj110  35187  cvxsconn  35630  btwnouttr2  36409  cgrxfr  36442  btwnxfr  36443  lineext  36463  segcon2  36492  brsegle2  36496  seglecgr12im  36497  segletr  36501  broutsideof3  36513  outsideofeu  36518  lineunray  36534  lineelsb2  36535  neibastop3  36758  ttcmin  36892  mh-inf3f1  36937  bj-imdiridlem  37712  isbasisrelowllem1  37884  isbasisrelowllem2  37885  fvineqsneu  37940  unccur  38137  fin2solem  38140  lindsadd  38147  matunitlindflem1  38150  matunitlindflem2  38151  poimirlem4  38158  poimirlem6  38160  poimirlem7  38161  poimirlem22  38176  poimirlem23  38177  poimirlem25  38179  poimirlem26  38180  poimirlem28  38182  poimirlem30  38184  poimirlem31  38185  poimirlem32  38186  poimir  38187  broucube  38188  heicant  38189  mblfinlem3  38193  volsupnfl  38199  itg2addnclem  38205  itg2addnclem2  38206  itg2addnclem3  38207  ftc1anclem1  38227  ftc1anclem5  38231  ftc1anclem6  38232  ftc1anc  38235  unirep  38248  filbcmb  38274  fzmul  38275  fdc  38279  nninfnub  38285  isbnd2  38317  bndss  38320  prdsbnd  38327  prdstotbnd  38328  ismtyres  38342  rrnmet  38363  rrncmslem  38366  rrnequiv  38369  ghomco  38425  grpokerinj  38427  rngonegmn1l  38475  isdrngo2  38492  rngoisocnv  38515  divrngidl  38562  intidl  38563  unichnidl  38565  prnc  38601  isfldidl  38602  cvrexchlem  40078  ps-2  40137  3atnelvolN  40245  dib1dim  41824  dib1dim2  41827  expeqidd  42971  evlselv  43208  fsuppind  43209  mzpindd  43364  dvdsabsmod0  43601  radcnvrat  44911  expgrowth  44932  modelac8prim  45588  fnchoice  45636  infxrbnd2  45971  infleinflem2  45973  xrralrecnnge  45992  limsuppnfdlem  46302  icccncfext  46488  dvnmul  46544  dvnprodlem2  46548  stoweidlem17  46618  stoweidlem30  46631  stoweidlem38  46639  stoweidlem42  46643  stoweidlem44  46645  fourierdlem31  46739  fourierdlem73  46780  fourierdlem74  46781  fourierdlem75  46782  fourierdlem83  46790  fourierdlem94  46801  fourierdlem113  46820  etransclem4  46839  hoicvr  47149  iinhoiicclem  47274  iccvonmbllem  47279  smfsuplem1  47412  smfsupdmmbllem  47445  smfinfdmmbllem  47449  itsclquadeu  49437  aacllem  50470