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  5661  ordintdif  6416  ordunisssuc  6473  fssres  6748  dffv2  6980  isocnv  7332  f1oiso  7353  f1ocnvfv3  7411  fiunlem  7941  mpof1o2d  8123  onfununi  8330  oev2  8510  oaordi  8533  oaass  8548  omlimcl  8565  odi  8566  omass  8567  oewordri  8580  oelim2  8583  oeoa  8585  oeoe  8587  nnaordi  8606  omabs  8639  eceqoveq  8822  mapxpen  9133  mapdom2  9138  findcard  9150  dif1ennnALT  9239  fimax2g  9248  isfinite2  9260  fimin2g  9461  rankval3b  9800  isf32lem9  10355  fin1a2s  10408  zornn0g  10499  gchen1  10620  gchen2  10621  intwun  10730  suplem2pr  11048  recexsrlem  11098  axpre-sup  11164  axsup  11295  dedekind  11383  recextlem2  11855  divne0  11894  dfinfre  12206  qreccl  13003  xrlttr  13175  xaddf  13260  xrsupsslem  13343  xrinfmsslem  13344  supxr2  13350  supxrunb1  13355  supxrbnd1  13357  supxrbnd2  13358  modid  13940  seqof  14106  cau3lem  15417  lo1bdd2  15586  o1co  15648  rlimcn3  15652  climcn1  15654  climcn2  15655  rlimsqzlem  15711  caucvgb  15742  fsumrlim  15874  fsumo1  15875  ntrivcvg  15962  rplpwr  16626  dvdssq  16635  nn0seqcvgd  16638  lcmgcdlem  16674  isprm6  16783  phiprmpw  16845  pcneg  16944  prmpwdvds  16974  4sqlem19  17033  0ramcl  17093  imasleval  17605  catpropd  17775  funcres2c  17970  initoeu2  18083  oduprs  18366  latdisdlem  18562  acsfiindd  18619  dirtr  18668  chnind  18687  mndpsuppss  18833  mndind  18897  grpinveu  19051  mulgnn0subcl  19163  mulgsubcl  19164  mhmmulg  19191  cycsubm  19283  cycsubgcl  19287  cycsubgss  19288  ghmmulg  19308  odf1  19642  dfod2  19644  gexdvds2  19665  sylow2blem3  19702  frgpup1  19855  iscyggen2  19961  iscyg3  19966  prdsgsum  20061  ringrghm  20407  pwsgprod  20422  dvdsrcl2  20459  crngunit  20471  dvdsrpropd  20509  isdrng3lem2  20867  lss1d  21099  quscrng  21438  ssdifidllem  21499  ssdifidlprm  21501  mulgghm2  21641  frgpcyg  21738  ip0r  21802  isphld  21819  frlmgsum  21937  uvcresum  21958  psdmul  22344  coe1tmmul  22453  mdetdiagid  22772  cpmatmcllem  22890  tgcl  23141  0ntr  23243  innei  23297  neitr  23352  ordtrest2lem  23375  cncnp  23452  cnnei  23454  2ndcdisj  23628  dislly  23669  dissnlocfin  23701  kgenss  23715  ptcnplem  23793  ptcnp  23794  ptcn  23799  cnmpt2k  23860  qtoprest  23889  kqt0lem  23908  isr0  23909  kqreglem1  23913  trfilss  24061  isufil2  24080  ufileu  24091  hausflim  24153  cnextcn  24239  symgtgp  24278  tsmssubm  24315  tsmsxplem1  24325  ustfilxp  24385  ustuqtop0  24412  elbl2ps  24561  elbl2  24562  nrginvrcn  24864  nmoix  24901  nmoleub  24903  cncfco  25081  icccvx  25124  iscmet3  25467  rrxmet  25582  ovolfioo  25641  ovolficc  25642  ovolicc2lem4  25694  iunmbl2  25731  dyadmax  25772  mbfsup  25838  mbflimsup  25840  mbflim  25842  itg1addlem4  25873  mbfi1flimlem  25896  itg2monolem1  25924  itg2mono  25927  itg2i1fseqle  25928  itg2i1fseq  25929  itg2addlem  25932  itg2gt0  25934  itg2cnlem1  25935  itgfsum  26001  cnlimc  26062  dvlip2  26169  itgsubst  26223  plyeq0lem  26382  plypf1  26384  dvtaylp  26548  ulmcaulem  26572  ulmcau  26573  ulmcn  26577  ulmdvlem3  26580  mtest  26582  pserulm  26600  pserdvlem2  26606  logdivlt  26801  advlogexp  26835  cxpexp  26848  cxpcl  26854  xrlimcnp  27148  basellem4  27263  logexprlim  27404  dchrsum2  27447  sumdchr2  27449  rpvmasum2  27691  pntrsumbnd2  27746  pntleml  27790  noreson  27839  z12zsodd  28690  tglineeltr  28919  plngrotlem2  29085  brbtwn2  29270  colinearalglem4  29274  axeuclidlem  29327  axcontlem8  29336  axcontlem10  29338  grpoidinvlem3  30873  grpoideu  30876  grpoinveu  30886  nmcvcn  31062  nmounbi  31143  blocnilem  31171  ubthlem1  31237  h2hlm  31347  ocsh  31650  brafnmul  32318  kbpj  32323  nmcexi  32393  lnconi  32400  riesz1  32432  mdbr2  32663  mdsl0  32677  mdslmd3i  32699  csmdsymi  32701  atcvatlem  32752  chirredlem1  32757  chirredi  32761  cdj3lem2b  32804  xrge0infss  33120  mgcmntco  33327  lmodvslmhm  33383  suppgsumssiun  33405  gsumwrd2dccatlem  33410  submarchi  33519  dvdsruasso  33711  grplsm0l  33725  ssmxidllem  33769  rprmndvdsru  33832  r1plmhm  33912  mplvrpmmhm  33949  mplvrpmrhm  33950  esplyfval1  33976  lindsunlem  34027  lindsun  34028  fldextrspunlsplem  34076  extdgfialglem2  34096  madjusmdetlem2  34231  zarcmplem  34284  ordtrest2NEWlem  34325  voliune  34632  fsum2dsub  35007  circlemeth  35040  bnj110  35259  cvxsconn  35747  btwnouttr2  36526  cgrxfr  36559  btwnxfr  36560  lineext  36580  segcon2  36609  brsegle2  36613  seglecgr12im  36614  segletr  36618  broutsideof3  36630  outsideofeu  36635  lineunray  36651  lineelsb2  36652  nmulrid  36701  neibastop3  36905  ttcmin  37039  mh-inf3f1  37084  bj-imdiridlem  37861  isbasisrelowllem1  38033  isbasisrelowllem2  38034  fvineqsneu  38089  unccur  38286  fin2solem  38289  lindsadd  38296  matunitlindflem1  38299  matunitlindflem2  38300  poimirlem4  38307  poimirlem6  38309  poimirlem7  38310  poimirlem22  38325  poimirlem23  38326  poimirlem25  38328  poimirlem26  38329  poimirlem28  38331  poimirlem30  38333  poimirlem31  38334  poimirlem32  38335  poimir  38336  broucube  38337  heicant  38338  mblfinlem3  38342  volsupnfl  38348  itg2addnclem  38354  itg2addnclem2  38355  itg2addnclem3  38356  ftc1anclem1  38376  ftc1anclem5  38380  ftc1anclem6  38381  ftc1anc  38384  unirep  38397  filbcmb  38423  fzmul  38424  fdc  38428  nninfnub  38434  isbnd2  38466  bndss  38469  prdsbnd  38476  prdstotbnd  38477  ismtyres  38491  rrnmet  38512  rrncmslem  38515  rrnequiv  38518  ghomco  38574  grpokerinj  38576  rngonegmn1l  38624  isdrngo2  38641  rngoisocnv  38664  divrngidl  38711  intidl  38712  unichnidl  38714  prnc  38750  isfldidl  38751  cvrexchlem  40225  ps-2  40284  3atnelvolN  40392  dib1dim  41971  dib1dim2  41974  expeqidd  43118  evlselv  43353  fsuppind  43354  mzpindd  43509  dvdsabsmod0  43746  radcnvrat  45056  expgrowth  45077  modelac8prim  45733  fnchoice  45781  infxrbnd2  46116  infleinflem2  46118  xrralrecnnge  46137  limsuppnfdlem  46447  icccncfext  46633  dvnmul  46689  dvnprodlem2  46693  stoweidlem17  46763  stoweidlem30  46776  stoweidlem38  46784  stoweidlem42  46788  stoweidlem44  46790  fourierdlem31  46884  fourierdlem73  46925  fourierdlem74  46926  fourierdlem75  46927  fourierdlem83  46935  fourierdlem94  46946  fourierdlem113  46965  etransclem4  46984  hoicvr  47294  iinhoiicclem  47419  iccvonmbllem  47424  smfsuplem1  47557  smfsupdmmbllem  47590  smfinfdmmbllem  47594  itsclquadeu  49589  aacllem  50653