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  5618  ordintdif  6365  ordunisssuc  6422  fssres  6697  dffv2  6926  isocnv  7273  f1oiso  7294  f1ocnvfv3  7350  fiunlem  7883  onfununi  8270  oev2  8447  oaordi  8470  oaass  8485  omlimcl  8502  odi  8503  omass  8504  oewordri  8516  oelim2  8519  oeoa  8521  oeoe  8523  nnaordi  8542  omabs  8575  eceqoveq  8755  mapxpen  9067  mapdom2  9072  findcard  9084  dif1ennnALT  9172  fimax2g  9181  isfinite2  9193  fimin2g  9394  rankval3b  9730  isf32lem9  10263  fin1a2s  10316  zornn0g  10407  gchen1  10527  gchen2  10528  intwun  10637  suplem2pr  10955  recexsrlem  11005  axpre-sup  11071  axsup  11199  dedekind  11287  recextlem2  11759  divne0  11799  dfinfre  12114  qreccl  12873  xrlttr  13045  xaddf  13130  xrsupsslem  13213  xrinfmsslem  13214  supxr2  13220  supxrunb1  13225  supxrbnd1  13227  supxrbnd2  13228  modid  13807  seqof  13973  cau3lem  15269  lo1bdd2  15438  o1co  15500  rlimcn3  15504  climcn1  15506  climcn2  15507  rlimsqzlem  15563  caucvgb  15594  fsumrlim  15725  fsumo1  15726  ntrivcvg  15811  rplpwr  16476  dvdssq  16485  nn0seqcvgd  16488  lcmgcdlem  16524  isprm6  16632  phiprmpw  16694  pcneg  16793  prmpwdvds  16823  4sqlem19  16882  0ramcl  16942  imasleval  17453  catpropd  17623  funcres2c  17818  initoeu2  17931  oduprs  18214  latdisdlem  18410  acsfiindd  18467  dirtr  18516  chnind  18535  mndpsuppss  18681  mndind  18744  grpinveu  18895  mulgnn0subcl  19008  mulgsubcl  19009  mhmmulg  19036  cycsubm  19122  cycsubgcl  19126  cycsubgss  19127  ghmmulg  19148  odf1  19482  dfod2  19484  gexdvds2  19505  sylow2blem3  19542  frgpup1  19695  iscyggen2  19801  iscyg3  19806  prdsgsum  19901  ringrghm  20239  pwsgprod  20256  dvdsrcl2  20293  crngunit  20305  dvdsrpropd  20343  lss1d  20905  quscrng  21229  mulgghm2  21422  frgpcyg  21519  ip0r  21583  isphld  21600  frlmgsum  21718  uvcresum  21739  psdmul  22100  coe1tmmul  22210  mdetdiagid  22535  cpmatmcllem  22653  tgcl  22904  0ntr  23006  innei  23060  neitr  23115  ordtrest2lem  23138  cncnp  23215  cnnei  23217  2ndcdisj  23391  dislly  23432  dissnlocfin  23464  kgenss  23478  ptcnplem  23556  ptcnp  23557  ptcn  23562  cnmpt2k  23623  qtoprest  23652  kqt0lem  23671  isr0  23672  kqreglem1  23676  trfilss  23824  isufil2  23843  ufileu  23854  hausflim  23916  cnextcn  24002  symgtgp  24041  tsmssubm  24078  tsmsxplem1  24088  ustfilxp  24148  ustuqtop0  24175  elbl2ps  24324  elbl2  24325  nrginvrcn  24627  nmoix  24664  nmoleub  24666  cncfco  24847  icccvx  24895  iscmet3  25240  rrxmet  25355  ovolfioo  25415  ovolficc  25416  ovolicc2lem4  25468  iunmbl2  25505  dyadmax  25546  mbfsup  25612  mbflimsup  25614  mbflim  25616  itg1addlem4  25647  mbfi1flimlem  25670  itg2monolem1  25698  itg2mono  25701  itg2i1fseqle  25702  itg2i1fseq  25703  itg2addlem  25706  itg2gt0  25708  itg2cnlem1  25709  itgfsum  25775  cnlimc  25836  dvlip2  25947  itgsubst  26003  plyeq0lem  26162  plypf1  26164  dvtaylp  26325  ulmcaulem  26350  ulmcau  26351  ulmcn  26355  ulmdvlem3  26358  mtest  26360  pserulm  26378  pserdvlem2  26385  logdivlt  26577  advlogexp  26611  cxpexp  26624  cxpcl  26630  xrlimcnp  26925  basellem4  27041  logexprlim  27183  dchrsum2  27226  sumdchr2  27228  rpvmasum2  27470  pntrsumbnd2  27525  pntleml  27569  noreson  27619  zs12zodd  28412  tglineeltr  28629  brbtwn2  28904  colinearalglem4  28908  axeuclidlem  28961  axcontlem8  28970  axcontlem10  28972  grpoidinvlem3  30507  grpoideu  30510  grpoinveu  30520  nmcvcn  30696  nmounbi  30777  blocnilem  30805  ubthlem1  30871  h2hlm  30981  ocsh  31284  brafnmul  31952  kbpj  31957  nmcexi  32027  lnconi  32034  riesz1  32066  mdbr2  32297  mdsl0  32311  mdslmd3i  32333  csmdsymi  32335  atcvatlem  32386  chirredlem1  32391  chirredi  32395  cdj3lem2b  32438  xrge0infss  32768  mgcmntco  33004  lmodvslmhm  33061  gsumwrd2dccatlem  33087  submarchi  33196  dvdsruasso  33394  grplsm0l  33412  ssdifidllem  33465  ssdifidlprm  33467  ssmxidllem  33482  rprmndvdsru  33538  r1plmhm  33619  mplvrpmmhm  33639  mplvrpmrhm  33640  lindsunlem  33709  lindsun  33710  fldextrspunlsplem  33758  extdgfialglem2  33778  madjusmdetlem2  33913  zarcmplem  33966  ordtrest2NEWlem  34007  voliune  34314  fsum2dsub  34692  circlemeth  34725  bnj110  34942  cvxsconn  35359  btwnouttr2  36138  cgrxfr  36171  btwnxfr  36172  lineext  36192  segcon2  36221  brsegle2  36225  seglecgr12im  36226  segletr  36230  broutsideof3  36242  outsideofeu  36247  lineunray  36263  lineelsb2  36264  neibastop3  36478  bj-imdiridlem  37302  isbasisrelowllem1  37472  isbasisrelowllem2  37473  fvineqsneu  37528  unccur  37716  fin2solem  37719  lindsadd  37726  matunitlindflem1  37729  matunitlindflem2  37730  poimirlem4  37737  poimirlem6  37739  poimirlem7  37740  poimirlem22  37755  poimirlem23  37756  poimirlem25  37758  poimirlem26  37759  poimirlem28  37761  poimirlem30  37763  poimirlem31  37764  poimirlem32  37765  poimir  37766  broucube  37767  heicant  37768  mblfinlem3  37772  volsupnfl  37778  itg2addnclem  37784  itg2addnclem2  37785  itg2addnclem3  37786  ftc1anclem1  37806  ftc1anclem5  37810  ftc1anclem6  37811  ftc1anc  37814  unirep  37827  filbcmb  37853  fzmul  37854  fdc  37858  nninfnub  37864  isbnd2  37896  bndss  37899  prdsbnd  37906  prdstotbnd  37907  ismtyres  37921  rrnmet  37942  rrncmslem  37945  rrnequiv  37948  ghomco  38004  grpokerinj  38006  rngonegmn1l  38054  isdrngo2  38071  rngoisocnv  38094  divrngidl  38141  intidl  38142  unichnidl  38144  prnc  38180  isfldidl  38181  cvrexchlem  39591  ps-2  39650  3atnelvolN  39758  dib1dim  41337  dib1dim2  41340  f1o2d2  42404  expeqidd  42495  evlselv  42745  fsuppind  42748  mzpindd  42903  dvdsabsmod0  43144  radcnvrat  44471  expgrowth  44492  modelac8prim  45149  fnchoice  45190  infxrbnd2  45529  infleinflem2  45531  xrralrecnnge  45550  limsuppnfdlem  45861  icccncfext  46047  dvnmul  46103  dvnprodlem2  46107  stoweidlem17  46177  stoweidlem30  46190  stoweidlem38  46198  stoweidlem42  46202  stoweidlem44  46204  fourierdlem31  46298  fourierdlem73  46339  fourierdlem74  46340  fourierdlem75  46341  fourierdlem83  46349  fourierdlem94  46360  fourierdlem113  46379  etransclem4  46398  iinhoiicclem  46833  iccvonmbllem  46838  smfsuplem1  46971  smfsupdmmbllem  47004  smfinfdmmbllem  47008  itsclquadeu  48939  aacllem  49962