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  5628  ordintdif  6371  ordunisssuc  6428  fssres  6708  dffv2  6938  isocnv  7287  f1oiso  7308  f1ocnvfv3  7364  fiunlem  7900  onfununi  8287  oev2  8464  oaordi  8487  oaass  8502  omlimcl  8519  odi  8520  omass  8521  oewordri  8533  oelim2  8536  oeoa  8538  oeoe  8540  nnaordi  8559  omabs  8592  eceqoveq  8772  mapxpen  9084  mapdom2  9089  findcard  9104  dif1ennnALT  9198  fimax2g  9209  isfinite2  9221  fimin2g  9426  rankval3b  9755  isf32lem9  10290  fin1a2s  10343  zornn0g  10434  gchen1  10554  gchen2  10555  intwun  10664  suplem2pr  10982  recexsrlem  11032  axpre-sup  11098  axsup  11225  dedekind  11313  recextlem2  11785  divne0  11825  dfinfre  12140  qreccl  12904  xrlttr  13076  xaddf  13160  xrsupsslem  13243  xrinfmsslem  13244  supxr2  13250  supxrunb1  13255  supxrbnd1  13257  supxrbnd2  13258  modid  13834  seqof  14000  cau3lem  15297  lo1bdd2  15466  o1co  15528  rlimcn3  15532  climcn1  15534  climcn2  15535  rlimsqzlem  15591  caucvgb  15622  fsumrlim  15753  fsumo1  15754  ntrivcvg  15839  rplpwr  16504  dvdssq  16513  nn0seqcvgd  16516  lcmgcdlem  16552  isprm6  16660  phiprmpw  16722  pcneg  16821  prmpwdvds  16851  4sqlem19  16910  0ramcl  16970  imasleval  17480  catpropd  17646  funcres2c  17841  initoeu2  17954  oduprs  18237  latdisdlem  18431  acsfiindd  18488  dirtr  18537  mndpsuppss  18668  mndind  18731  grpinveu  18882  mulgnn0subcl  18995  mulgsubcl  18996  mhmmulg  19023  cycsubm  19110  cycsubgcl  19114  cycsubgss  19115  ghmmulg  19136  odf1  19468  dfod2  19470  gexdvds2  19491  sylow2blem3  19528  frgpup1  19681  iscyggen2  19787  iscyg3  19792  prdsgsum  19887  ringrghm  20198  dvdsrcl2  20251  crngunit  20263  dvdsrpropd  20301  lss1d  20845  quscrng  21169  mulgghm2  21362  frgpcyg  21459  ip0r  21522  isphld  21539  frlmgsum  21657  uvcresum  21678  psdmul  22029  coe1tmmul  22139  mdetdiagid  22463  cpmatmcllem  22581  tgcl  22832  0ntr  22934  innei  22988  neitr  23043  ordtrest2lem  23066  cncnp  23143  cnnei  23145  2ndcdisj  23319  dislly  23360  dissnlocfin  23392  kgenss  23406  ptcnplem  23484  ptcnp  23485  ptcn  23490  cnmpt2k  23551  qtoprest  23580  kqt0lem  23599  isr0  23600  kqreglem1  23604  trfilss  23752  isufil2  23771  ufileu  23782  hausflim  23844  cnextcn  23930  symgtgp  23969  tsmssubm  24006  tsmsxplem1  24016  ustfilxp  24076  ustuqtop0  24104  elbl2ps  24253  elbl2  24254  nrginvrcn  24556  nmoix  24593  nmoleub  24595  cncfco  24776  icccvx  24824  iscmet3  25169  rrxmet  25284  ovolfioo  25344  ovolficc  25345  ovolicc2lem4  25397  iunmbl2  25434  dyadmax  25475  mbfsup  25541  mbflimsup  25543  mbflim  25545  itg1addlem4  25576  mbfi1flimlem  25599  itg2monolem1  25627  itg2mono  25630  itg2i1fseqle  25631  itg2i1fseq  25632  itg2addlem  25635  itg2gt0  25637  itg2cnlem1  25638  itgfsum  25704  cnlimc  25765  dvlip2  25876  itgsubst  25932  plyeq0lem  26091  plypf1  26093  dvtaylp  26254  ulmcaulem  26279  ulmcau  26280  ulmcn  26284  ulmdvlem3  26287  mtest  26289  pserulm  26307  pserdvlem2  26314  logdivlt  26506  advlogexp  26540  cxpexp  26553  cxpcl  26559  xrlimcnp  26854  basellem4  26970  logexprlim  27112  dchrsum2  27155  sumdchr2  27157  rpvmasum2  27399  pntrsumbnd2  27454  pntleml  27498  noreson  27548  tglineeltr  28534  brbtwn2  28808  colinearalglem4  28812  axeuclidlem  28865  axcontlem8  28874  axcontlem10  28876  grpoidinvlem3  30408  grpoideu  30411  grpoinveu  30421  nmcvcn  30597  nmounbi  30678  blocnilem  30706  ubthlem1  30772  h2hlm  30882  ocsh  31185  brafnmul  31853  kbpj  31858  nmcexi  31928  lnconi  31935  riesz1  31967  mdbr2  32198  mdsl0  32212  mdslmd3i  32234  csmdsymi  32236  atcvatlem  32287  chirredlem1  32292  chirredi  32296  cdj3lem2b  32339  xrge0infss  32656  mgcmntco  32893  chnind  32910  lmodvslmhm  32963  gsumwrd2dccatlem  32979  submarchi  33113  dvdsruasso  33329  grplsm0l  33347  ssdifidllem  33400  ssdifidlprm  33402  ssmxidllem  33417  rprmndvdsru  33473  r1plmhm  33548  lindsunlem  33593  lindsun  33594  fldextrspunlsplem  33641  madjusmdetlem2  33791  zarcmplem  33844  ordtrest2NEWlem  33885  voliune  34192  fsum2dsub  34571  circlemeth  34604  bnj110  34821  cvxsconn  35203  btwnouttr2  35983  cgrxfr  36016  btwnxfr  36017  lineext  36037  segcon2  36066  brsegle2  36070  seglecgr12im  36071  segletr  36075  broutsideof3  36087  outsideofeu  36092  lineunray  36108  lineelsb2  36109  neibastop3  36323  bj-imdiridlem  37146  isbasisrelowllem1  37316  isbasisrelowllem2  37317  fvineqsneu  37372  unccur  37570  fin2solem  37573  lindsadd  37580  matunitlindflem1  37583  matunitlindflem2  37584  poimirlem4  37591  poimirlem6  37593  poimirlem7  37594  poimirlem22  37609  poimirlem23  37610  poimirlem25  37612  poimirlem26  37613  poimirlem28  37615  poimirlem30  37617  poimirlem31  37618  poimirlem32  37619  poimir  37620  broucube  37621  heicant  37622  mblfinlem3  37626  volsupnfl  37632  itg2addnclem  37638  itg2addnclem2  37639  itg2addnclem3  37640  ftc1anclem1  37660  ftc1anclem5  37664  ftc1anclem6  37665  ftc1anc  37668  unirep  37681  filbcmb  37707  fzmul  37708  fdc  37712  nninfnub  37718  isbnd2  37750  bndss  37753  prdsbnd  37760  prdstotbnd  37761  ismtyres  37775  rrnmet  37796  rrncmslem  37799  rrnequiv  37802  ghomco  37858  grpokerinj  37860  rngonegmn1l  37908  isdrngo2  37925  rngoisocnv  37948  divrngidl  37995  intidl  37996  unichnidl  37998  prnc  38034  isfldidl  38035  cvrexchlem  39386  ps-2  39445  3atnelvolN  39553  dib1dim  41132  dib1dim2  41135  f1o2d2  42194  expeqidd  42286  pwsgprod  42505  evlselv  42548  fsuppind  42551  mzpindd  42707  dvdsabsmod0  42949  radcnvrat  44276  expgrowth  44297  modelac8prim  44955  fnchoice  44996  infxrbnd2  45338  infleinflem2  45340  xrralrecnnge  45359  limsuppnfdlem  45672  icccncfext  45858  dvnmul  45914  dvnprodlem2  45918  stoweidlem17  45988  stoweidlem30  46001  stoweidlem38  46009  stoweidlem42  46013  stoweidlem44  46015  fourierdlem31  46109  fourierdlem73  46150  fourierdlem74  46151  fourierdlem75  46152  fourierdlem83  46160  fourierdlem94  46171  fourierdlem113  46190  etransclem4  46209  iinhoiicclem  46644  iccvonmbllem  46649  smfsuplem1  46782  smfsupdmmbllem  46815  smfinfdmmbllem  46819  itsclquadeu  48739  aacllem  49763