Theorem an32s 653

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 647	. 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  656  anabss1  667  biadanid  823  wereu2  5629  ordintdif  6376  ordunisssuc  6433  fssres  6708  dffv2  6937  isocnv  7286  f1oiso  7307  f1ocnvfv3  7363  fiunlem  7896  onfununi  8283  oev2  8460  oaordi  8483  oaass  8498  omlimcl  8515  odi  8516  omass  8517  oewordri  8530  oelim2  8533  oeoa  8535  oeoe  8537  nnaordi  8556  omabs  8589  eceqoveq  8771  mapxpen  9083  mapdom2  9088  findcard  9100  dif1ennnALT  9189  fimax2g  9198  isfinite2  9210  fimin2g  9414  rankval3b  9750  isf32lem9  10283  fin1a2s  10336  zornn0g  10427  gchen1  10548  gchen2  10549  intwun  10658  suplem2pr  10976  recexsrlem  11026  axpre-sup  11092  axsup  11220  dedekind  11308  recextlem2  11780  divne0  11820  dfinfre  12135  qreccl  12894  xrlttr  13066  xaddf  13151  xrsupsslem  13234  xrinfmsslem  13235  supxr2  13241  supxrunb1  13246  supxrbnd1  13248  supxrbnd2  13249  modid  13828  seqof  13994  cau3lem  15290  lo1bdd2  15459  o1co  15521  rlimcn3  15525  climcn1  15527  climcn2  15528  rlimsqzlem  15584  caucvgb  15615  fsumrlim  15746  fsumo1  15747  ntrivcvg  15832  rplpwr  16497  dvdssq  16506  nn0seqcvgd  16509  lcmgcdlem  16545  isprm6  16653  phiprmpw  16715  pcneg  16814  prmpwdvds  16844  4sqlem19  16903  0ramcl  16963  imasleval  17474  catpropd  17644  funcres2c  17839  initoeu2  17952  oduprs  18235  latdisdlem  18431  acsfiindd  18488  dirtr  18537  chnind  18556  mndpsuppss  18702  mndind  18765  grpinveu  18916  mulgnn0subcl  19029  mulgsubcl  19030  mhmmulg  19057  cycsubm  19143  cycsubgcl  19147  cycsubgss  19148  ghmmulg  19169  odf1  19503  dfod2  19505  gexdvds2  19526  sylow2blem3  19563  frgpup1  19716  iscyggen2  19822  iscyg3  19827  prdsgsum  19922  ringrghm  20260  pwsgprod  20277  dvdsrcl2  20314  crngunit  20326  dvdsrpropd  20364  lss1d  20926  quscrng  21250  mulgghm2  21443  frgpcyg  21540  ip0r  21604  isphld  21621  frlmgsum  21739  uvcresum  21760  psdmul  22121  coe1tmmul  22231  mdetdiagid  22556  cpmatmcllem  22674  tgcl  22925  0ntr  23027  innei  23081  neitr  23136  ordtrest2lem  23159  cncnp  23236  cnnei  23238  2ndcdisj  23412  dislly  23453  dissnlocfin  23485  kgenss  23499  ptcnplem  23577  ptcnp  23578  ptcn  23583  cnmpt2k  23644  qtoprest  23673  kqt0lem  23692  isr0  23693  kqreglem1  23697  trfilss  23845  isufil2  23864  ufileu  23875  hausflim  23937  cnextcn  24023  symgtgp  24062  tsmssubm  24099  tsmsxplem1  24109  ustfilxp  24169  ustuqtop0  24196  elbl2ps  24345  elbl2  24346  nrginvrcn  24648  nmoix  24685  nmoleub  24687  cncfco  24868  icccvx  24916  iscmet3  25261  rrxmet  25376  ovolfioo  25436  ovolficc  25437  ovolicc2lem4  25489  iunmbl2  25526  dyadmax  25567  mbfsup  25633  mbflimsup  25635  mbflim  25637  itg1addlem4  25668  mbfi1flimlem  25691  itg2monolem1  25719  itg2mono  25722  itg2i1fseqle  25723  itg2i1fseq  25724  itg2addlem  25727  itg2gt0  25729  itg2cnlem1  25730  itgfsum  25796  cnlimc  25857  dvlip2  25968  itgsubst  26024  plyeq0lem  26183  plypf1  26185  dvtaylp  26346  ulmcaulem  26371  ulmcau  26372  ulmcn  26376  ulmdvlem3  26379  mtest  26381  pserulm  26399  pserdvlem2  26406  logdivlt  26598  advlogexp  26632  cxpexp  26645  cxpcl  26651  xrlimcnp  26946  basellem4  27062  logexprlim  27204  dchrsum2  27247  sumdchr2  27249  rpvmasum2  27491  pntrsumbnd2  27546  pntleml  27590  noreson  27640  z12zsodd  28490  tglineeltr  28715  brbtwn2  28990  colinearalglem4  28994  axeuclidlem  29047  axcontlem8  29056  axcontlem10  29058  grpoidinvlem3  30594  grpoideu  30597  grpoinveu  30607  nmcvcn  30783  nmounbi  30864  blocnilem  30892  ubthlem1  30958  h2hlm  31068  ocsh  31371  brafnmul  32039  kbpj  32044  nmcexi  32114  lnconi  32121  riesz1  32153  mdbr2  32384  mdsl0  32398  mdslmd3i  32420  csmdsymi  32422  atcvatlem  32473  chirredlem1  32478  chirredi  32482  cdj3lem2b  32525  xrge0infss  32851  mgcmntco  33087  lmodvslmhm  33144  suppgsumssiun  33166  gsumwrd2dccatlem  33171  submarchi  33280  dvdsruasso  33478  grplsm0l  33496  ssdifidllem  33549  ssdifidlprm  33551  ssmxidllem  33566  rprmndvdsru  33622  r1plmhm  33703  mplvrpmmhm  33723  mplvrpmrhm  33724  esplyfval1  33750  lindsunlem  33802  lindsun  33803  fldextrspunlsplem  33851  extdgfialglem2  33871  madjusmdetlem2  34006  zarcmplem  34059  ordtrest2NEWlem  34100  voliune  34407  fsum2dsub  34785  circlemeth  34818  bnj110  35034  cvxsconn  35459  btwnouttr2  36238  cgrxfr  36271  btwnxfr  36272  lineext  36292  segcon2  36321  brsegle2  36325  seglecgr12im  36326  segletr  36330  broutsideof3  36342  outsideofeu  36347  lineunray  36363  lineelsb2  36364  neibastop3  36578  bj-imdiridlem  37440  isbasisrelowllem1  37610  isbasisrelowllem2  37611  fvineqsneu  37666  unccur  37854  fin2solem  37857  lindsadd  37864  matunitlindflem1  37867  matunitlindflem2  37868  poimirlem4  37875  poimirlem6  37877  poimirlem7  37878  poimirlem22  37893  poimirlem23  37894  poimirlem25  37896  poimirlem26  37897  poimirlem28  37899  poimirlem30  37901  poimirlem31  37902  poimirlem32  37903  poimir  37904  broucube  37905  heicant  37906  mblfinlem3  37910  volsupnfl  37916  itg2addnclem  37922  itg2addnclem2  37923  itg2addnclem3  37924  ftc1anclem1  37944  ftc1anclem5  37948  ftc1anclem6  37949  ftc1anc  37952  unirep  37965  filbcmb  37991  fzmul  37992  fdc  37996  nninfnub  38002  isbnd2  38034  bndss  38037  prdsbnd  38044  prdstotbnd  38045  ismtyres  38059  rrnmet  38080  rrncmslem  38083  rrnequiv  38086  ghomco  38142  grpokerinj  38144  rngonegmn1l  38192  isdrngo2  38209  rngoisocnv  38232  divrngidl  38279  intidl  38280  unichnidl  38282  prnc  38318  isfldidl  38319  cvrexchlem  39795  ps-2  39854  3atnelvolN  39962  dib1dim  41541  dib1dim2  41544  f1o2d2  42605  expeqidd  42695  evlselv  42945  fsuppind  42948  mzpindd  43103  dvdsabsmod0  43344  radcnvrat  44670  expgrowth  44691  modelac8prim  45348  fnchoice  45389  infxrbnd2  45727  infleinflem2  45729  xrralrecnnge  45748  limsuppnfdlem  46059  icccncfext  46245  dvnmul  46301  dvnprodlem2  46305  stoweidlem17  46375  stoweidlem30  46388  stoweidlem38  46396  stoweidlem42  46400  stoweidlem44  46402  fourierdlem31  46496  fourierdlem73  46537  fourierdlem74  46538  fourierdlem75  46539  fourierdlem83  46547  fourierdlem94  46558  fourierdlem113  46577  etransclem4  46596  iinhoiicclem  47031  iccvonmbllem  47036  smfsuplem1  47169  smfsupdmmbllem  47202  smfinfdmmbllem  47206  itsclquadeu  49137  aacllem  50160