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  5635  ordintdif  6383  ordunisssuc  6440  fssres  6726  dffv2  6956  isocnv  7305  f1oiso  7326  f1ocnvfv3  7382  fiunlem  7920  onfununi  8310  oev2  8487  oaordi  8510  oaass  8525  omlimcl  8542  odi  8543  omass  8544  oewordri  8556  oelim2  8559  oeoa  8561  oeoe  8563  nnaordi  8582  omabs  8615  eceqoveq  8795  mapxpen  9107  mapdom2  9112  findcard  9127  dif1ennnALT  9222  fimax2g  9233  isfinite2  9245  fimin2g  9450  rankval3b  9779  isf32lem9  10314  fin1a2s  10367  zornn0g  10458  gchen1  10578  gchen2  10579  intwun  10688  suplem2pr  11006  recexsrlem  11056  axpre-sup  11122  axsup  11249  dedekind  11337  recextlem2  11809  divne0  11849  dfinfre  12164  qreccl  12928  xrlttr  13100  xaddf  13184  xrsupsslem  13267  xrinfmsslem  13268  supxr2  13274  supxrunb1  13279  supxrbnd1  13281  supxrbnd2  13282  modid  13858  seqof  14024  cau3lem  15321  lo1bdd2  15490  o1co  15552  rlimcn3  15556  climcn1  15558  climcn2  15559  rlimsqzlem  15615  caucvgb  15646  fsumrlim  15777  fsumo1  15778  ntrivcvg  15863  rplpwr  16528  dvdssq  16537  nn0seqcvgd  16540  lcmgcdlem  16576  isprm6  16684  phiprmpw  16746  pcneg  16845  prmpwdvds  16875  4sqlem19  16934  0ramcl  16994  imasleval  17504  catpropd  17670  funcres2c  17865  initoeu2  17978  oduprs  18261  latdisdlem  18455  acsfiindd  18512  dirtr  18561  mndpsuppss  18692  mndind  18755  grpinveu  18906  mulgnn0subcl  19019  mulgsubcl  19020  mhmmulg  19047  cycsubm  19134  cycsubgcl  19138  cycsubgss  19139  ghmmulg  19160  odf1  19492  dfod2  19494  gexdvds2  19515  sylow2blem3  19552  frgpup1  19705  iscyggen2  19811  iscyg3  19816  prdsgsum  19911  ringrghm  20222  dvdsrcl2  20275  crngunit  20287  dvdsrpropd  20325  lss1d  20869  quscrng  21193  mulgghm2  21386  frgpcyg  21483  ip0r  21546  isphld  21563  frlmgsum  21681  uvcresum  21702  psdmul  22053  coe1tmmul  22163  mdetdiagid  22487  cpmatmcllem  22605  tgcl  22856  0ntr  22958  innei  23012  neitr  23067  ordtrest2lem  23090  cncnp  23167  cnnei  23169  2ndcdisj  23343  dislly  23384  dissnlocfin  23416  kgenss  23430  ptcnplem  23508  ptcnp  23509  ptcn  23514  cnmpt2k  23575  qtoprest  23604  kqt0lem  23623  isr0  23624  kqreglem1  23628  trfilss  23776  isufil2  23795  ufileu  23806  hausflim  23868  cnextcn  23954  symgtgp  23993  tsmssubm  24030  tsmsxplem1  24040  ustfilxp  24100  ustuqtop0  24128  elbl2ps  24277  elbl2  24278  nrginvrcn  24580  nmoix  24617  nmoleub  24619  cncfco  24800  icccvx  24848  iscmet3  25193  rrxmet  25308  ovolfioo  25368  ovolficc  25369  ovolicc2lem4  25421  iunmbl2  25458  dyadmax  25499  mbfsup  25565  mbflimsup  25567  mbflim  25569  itg1addlem4  25600  mbfi1flimlem  25623  itg2monolem1  25651  itg2mono  25654  itg2i1fseqle  25655  itg2i1fseq  25656  itg2addlem  25659  itg2gt0  25661  itg2cnlem1  25662  itgfsum  25728  cnlimc  25789  dvlip2  25900  itgsubst  25956  plyeq0lem  26115  plypf1  26117  dvtaylp  26278  ulmcaulem  26303  ulmcau  26304  ulmcn  26308  ulmdvlem3  26311  mtest  26313  pserulm  26331  pserdvlem2  26338  logdivlt  26530  advlogexp  26564  cxpexp  26577  cxpcl  26583  xrlimcnp  26878  basellem4  26994  logexprlim  27136  dchrsum2  27179  sumdchr2  27181  rpvmasum2  27423  pntrsumbnd2  27478  pntleml  27522  noreson  27572  tglineeltr  28558  brbtwn2  28832  colinearalglem4  28836  axeuclidlem  28889  axcontlem8  28898  axcontlem10  28900  grpoidinvlem3  30435  grpoideu  30438  grpoinveu  30448  nmcvcn  30624  nmounbi  30705  blocnilem  30733  ubthlem1  30799  h2hlm  30909  ocsh  31212  brafnmul  31880  kbpj  31885  nmcexi  31955  lnconi  31962  riesz1  31994  mdbr2  32225  mdsl0  32239  mdslmd3i  32261  csmdsymi  32263  atcvatlem  32314  chirredlem1  32319  chirredi  32323  cdj3lem2b  32366  xrge0infss  32683  mgcmntco  32920  chnind  32937  lmodvslmhm  32990  gsumwrd2dccatlem  33006  submarchi  33140  dvdsruasso  33356  grplsm0l  33374  ssdifidllem  33427  ssdifidlprm  33429  ssmxidllem  33444  rprmndvdsru  33500  r1plmhm  33575  lindsunlem  33620  lindsun  33621  fldextrspunlsplem  33668  madjusmdetlem2  33818  zarcmplem  33871  ordtrest2NEWlem  33912  voliune  34219  fsum2dsub  34598  circlemeth  34631  bnj110  34848  cvxsconn  35230  btwnouttr2  36010  cgrxfr  36043  btwnxfr  36044  lineext  36064  segcon2  36093  brsegle2  36097  seglecgr12im  36098  segletr  36102  broutsideof3  36114  outsideofeu  36119  lineunray  36135  lineelsb2  36136  neibastop3  36350  bj-imdiridlem  37173  isbasisrelowllem1  37343  isbasisrelowllem2  37344  fvineqsneu  37399  unccur  37597  fin2solem  37600  lindsadd  37607  matunitlindflem1  37610  matunitlindflem2  37611  poimirlem4  37618  poimirlem6  37620  poimirlem7  37621  poimirlem22  37636  poimirlem23  37637  poimirlem25  37639  poimirlem26  37640  poimirlem28  37642  poimirlem30  37644  poimirlem31  37645  poimirlem32  37646  poimir  37647  broucube  37648  heicant  37649  mblfinlem3  37653  volsupnfl  37659  itg2addnclem  37665  itg2addnclem2  37666  itg2addnclem3  37667  ftc1anclem1  37687  ftc1anclem5  37691  ftc1anclem6  37692  ftc1anc  37695  unirep  37708  filbcmb  37734  fzmul  37735  fdc  37739  nninfnub  37745  isbnd2  37777  bndss  37780  prdsbnd  37787  prdstotbnd  37788  ismtyres  37802  rrnmet  37823  rrncmslem  37826  rrnequiv  37829  ghomco  37885  grpokerinj  37887  rngonegmn1l  37935  isdrngo2  37952  rngoisocnv  37975  divrngidl  38022  intidl  38023  unichnidl  38025  prnc  38061  isfldidl  38062  cvrexchlem  39413  ps-2  39472  3atnelvolN  39580  dib1dim  41159  dib1dim2  41162  f1o2d2  42221  expeqidd  42313  pwsgprod  42532  evlselv  42575  fsuppind  42578  mzpindd  42734  dvdsabsmod0  42976  radcnvrat  44303  expgrowth  44324  modelac8prim  44982  fnchoice  45023  infxrbnd2  45365  infleinflem2  45367  xrralrecnnge  45386  limsuppnfdlem  45699  icccncfext  45885  dvnmul  45941  dvnprodlem2  45945  stoweidlem17  46015  stoweidlem30  46028  stoweidlem38  46036  stoweidlem42  46040  stoweidlem44  46042  fourierdlem31  46136  fourierdlem73  46177  fourierdlem74  46178  fourierdlem75  46179  fourierdlem83  46187  fourierdlem94  46198  fourierdlem113  46217  etransclem4  46236  iinhoiicclem  46671  iccvonmbllem  46676  smfsuplem1  46809  smfsupdmmbllem  46842  smfinfdmmbllem  46846  itsclquadeu  48766  aacllem  49790