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  5651  ordintdif  6403  ordunisssuc  6459  fssres  6743  dffv2  6973  isocnv  7322  f1oiso  7343  f1ocnvfv3  7398  fiunlem  7938  onfununi  8353  oev2  8533  oaordi  8556  oaass  8571  omlimcl  8588  odi  8589  omass  8590  oewordri  8602  oelim2  8605  oeoa  8607  oeoe  8609  nnaordi  8628  omabs  8661  eceqoveq  8834  mapxpen  9155  mapdom2  9160  findcard  9175  dif1ennnALT  9281  fimax2g  9292  isfinite2  9304  fimin2g  9509  rankval3b  9838  isf32lem9  10373  fin1a2s  10426  zornn0g  10517  gchen1  10637  gchen2  10638  intwun  10747  suplem2pr  11065  recexsrlem  11115  axpre-sup  11181  axsup  11308  dedekind  11396  recextlem2  11866  divne0  11906  dfinfre  12221  qreccl  12983  xrlttr  13154  xaddf  13238  xrsupsslem  13321  xrinfmsslem  13322  supxr2  13328  supxrunb1  13333  supxrbnd1  13335  supxrbnd2  13336  modid  13911  seqof  14075  cau3lem  15371  lo1bdd2  15538  o1co  15600  rlimcn3  15604  climcn1  15606  climcn2  15607  rlimsqzlem  15663  caucvgb  15694  fsumrlim  15825  fsumo1  15826  ntrivcvg  15911  rplpwr  16575  dvdssq  16584  nn0seqcvgd  16587  lcmgcdlem  16623  isprm6  16731  phiprmpw  16793  pcneg  16892  prmpwdvds  16922  4sqlem19  16981  0ramcl  17041  imasleval  17553  catpropd  17719  funcres2c  17914  initoeu2  18027  oduprs  18310  latdisdlem  18504  acsfiindd  18561  dirtr  18610  mndpsuppss  18741  mndind  18804  grpinveu  18955  mulgnn0subcl  19068  mulgsubcl  19069  mhmmulg  19096  cycsubm  19183  cycsubgcl  19187  cycsubgss  19188  ghmmulg  19209  odf1  19541  dfod2  19543  gexdvds2  19564  sylow2blem3  19601  frgpup1  19754  iscyggen2  19860  iscyg3  19865  prdsgsum  19960  ringrghm  20271  dvdsrcl2  20324  crngunit  20336  dvdsrpropd  20374  lss1d  20918  quscrng  21242  mulgghm2  21435  frgpcyg  21532  ip0r  21595  isphld  21612  frlmgsum  21730  uvcresum  21751  psdmul  22102  coe1tmmul  22212  mdetdiagid  22536  cpmatmcllem  22654  tgcl  22905  0ntr  23007  innei  23061  neitr  23116  ordtrest2lem  23139  cncnp  23216  cnnei  23218  2ndcdisj  23392  dislly  23433  dissnlocfin  23465  kgenss  23479  ptcnplem  23557  ptcnp  23558  ptcn  23563  cnmpt2k  23624  qtoprest  23653  kqt0lem  23672  isr0  23673  kqreglem1  23677  trfilss  23825  isufil2  23844  ufileu  23855  hausflim  23917  cnextcn  24003  symgtgp  24042  tsmssubm  24079  tsmsxplem1  24089  ustfilxp  24149  ustuqtop0  24177  elbl2ps  24326  elbl2  24327  nrginvrcn  24629  nmoix  24666  nmoleub  24668  cncfco  24849  icccvx  24897  iscmet3  25243  rrxmet  25358  ovolfioo  25418  ovolficc  25419  ovolicc2lem4  25471  iunmbl2  25508  dyadmax  25549  mbfsup  25615  mbflimsup  25617  mbflim  25619  itg1addlem4  25650  mbfi1flimlem  25673  itg2monolem1  25701  itg2mono  25704  itg2i1fseqle  25705  itg2i1fseq  25706  itg2addlem  25709  itg2gt0  25711  itg2cnlem1  25712  itgfsum  25778  cnlimc  25839  dvlip2  25950  itgsubst  26006  plyeq0lem  26165  plypf1  26167  dvtaylp  26328  ulmcaulem  26353  ulmcau  26354  ulmcn  26358  ulmdvlem3  26361  mtest  26363  pserulm  26381  pserdvlem2  26388  logdivlt  26580  advlogexp  26614  cxpexp  26627  cxpcl  26633  xrlimcnp  26928  basellem4  27044  logexprlim  27186  dchrsum2  27229  sumdchr2  27231  rpvmasum2  27473  pntrsumbnd2  27528  pntleml  27572  noreson  27622  tglineeltr  28556  brbtwn2  28830  colinearalglem4  28834  axeuclidlem  28887  axcontlem8  28896  axcontlem10  28898  grpoidinvlem3  30433  grpoideu  30436  grpoinveu  30446  nmcvcn  30622  nmounbi  30703  blocnilem  30731  ubthlem1  30797  h2hlm  30907  ocsh  31210  brafnmul  31878  kbpj  31883  nmcexi  31953  lnconi  31960  riesz1  31992  mdbr2  32223  mdsl0  32237  mdslmd3i  32259  csmdsymi  32261  atcvatlem  32312  chirredlem1  32317  chirredi  32321  cdj3lem2b  32364  xrge0infss  32683  mgcmntco  32920  chnind  32937  lmodvslmhm  32990  gsumwrd2dccatlem  33006  submarchi  33130  dvdsruasso  33346  grplsm0l  33364  ssdifidllem  33417  ssdifidlprm  33419  ssmxidllem  33434  rprmndvdsru  33490  r1plmhm  33565  lindsunlem  33610  lindsun  33611  fldextrspunlsplem  33660  madjusmdetlem2  33805  zarcmplem  33858  ordtrest2NEWlem  33899  voliune  34206  fsum2dsub  34585  circlemeth  34618  bnj110  34835  cvxsconn  35211  btwnouttr2  35986  cgrxfr  36019  btwnxfr  36020  lineext  36040  segcon2  36069  brsegle2  36073  seglecgr12im  36074  segletr  36078  broutsideof3  36090  outsideofeu  36095  lineunray  36111  lineelsb2  36112  neibastop3  36326  bj-imdiridlem  37149  isbasisrelowllem1  37319  isbasisrelowllem2  37320  fvineqsneu  37375  unccur  37573  fin2solem  37576  lindsadd  37583  matunitlindflem1  37586  matunitlindflem2  37587  poimirlem4  37594  poimirlem6  37596  poimirlem7  37597  poimirlem22  37612  poimirlem23  37613  poimirlem25  37615  poimirlem26  37616  poimirlem28  37618  poimirlem30  37620  poimirlem31  37621  poimirlem32  37622  poimir  37623  broucube  37624  heicant  37625  mblfinlem3  37629  volsupnfl  37635  itg2addnclem  37641  itg2addnclem2  37642  itg2addnclem3  37643  ftc1anclem1  37663  ftc1anclem5  37667  ftc1anclem6  37668  ftc1anc  37671  unirep  37684  filbcmb  37710  fzmul  37711  fdc  37715  nninfnub  37721  isbnd2  37753  bndss  37756  prdsbnd  37763  prdstotbnd  37764  ismtyres  37778  rrnmet  37799  rrncmslem  37802  rrnequiv  37805  ghomco  37861  grpokerinj  37863  rngonegmn1l  37911  isdrngo2  37928  rngoisocnv  37951  divrngidl  37998  intidl  37999  unichnidl  38001  prnc  38037  isfldidl  38038  cvrexchlem  39384  ps-2  39443  3atnelvolN  39551  dib1dim  41130  dib1dim2  41133  f1o2d2  42231  expeqidd  42321  pwsgprod  42514  evlselv  42557  fsuppind  42560  mzpindd  42716  dvdsabsmod0  42958  radcnvrat  44286  expgrowth  44307  modelac8prim  44965  fnchoice  45001  infxrbnd2  45344  infleinflem2  45346  xrralrecnnge  45365  limsuppnfdlem  45678  icccncfext  45864  dvnmul  45920  dvnprodlem2  45924  stoweidlem17  45994  stoweidlem30  46007  stoweidlem38  46015  stoweidlem42  46019  stoweidlem44  46021  fourierdlem31  46115  fourierdlem73  46156  fourierdlem74  46157  fourierdlem75  46158  fourierdlem83  46166  fourierdlem94  46177  fourierdlem113  46196  etransclem4  46215  iinhoiicclem  46650  iccvonmbllem  46655  smfsuplem1  46788  smfsupdmmbllem  46821  smfinfdmmbllem  46825  itsclquadeu  48705  aacllem  49613