Theorem an32s 664

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 658	. 2 ⊢ (((𝜑 ∧ 𝜒) ∧ 𝜓) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒))
2		an32s.1	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
3	1, 2	sylbi 220	1 ⊢ (((𝜑 ∧ 𝜒) ∧ 𝜓) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  anass1rs  667  anabss1  678  biadanid  834  wereu2  5658  ordintdif  6412  ordunisssuc  6469  fssres  6744  dffv2  6976  isocnv  7328  f1oiso  7349  f1ocnvfv3  7405  fiunlem  7935  mpof1o2d  8117  onfununi  8324  oev2  8504  oaordi  8527  oaass  8542  omlimcl  8559  odi  8560  omass  8561  oewordri  8574  oelim2  8577  oeoa  8579  oeoe  8581  nnaordi  8600  omabs  8633  eceqoveq  8816  mapxpen  9127  mapdom2  9132  findcard  9144  dif1ennnALT  9233  fimax2g  9242  isfinite2  9254  fimin2g  9455  rankval3b  9794  isf32lem9  10340  fin1a2s  10393  zornn0g  10484  gchen1  10605  gchen2  10606  intwun  10715  suplem2pr  11033  recexsrlem  11083  axpre-sup  11149  axsup  11280  dedekind  11368  recextlem2  11840  divne0  11879  dfinfre  12191  qreccl  12988  xrlttr  13160  xaddf  13245  xrsupsslem  13328  xrinfmsslem  13329  supxr2  13335  supxrunb1  13340  supxrbnd1  13342  supxrbnd2  13343  modid  13925  seqof  14091  cau3lem  15402  lo1bdd2  15571  o1co  15633  rlimcn3  15637  climcn1  15639  climcn2  15640  rlimsqzlem  15696  caucvgb  15727  fsumrlim  15859  fsumo1  15860  ntrivcvg  15947  rplpwr  16611  dvdssq  16620  nn0seqcvgd  16623  lcmgcdlem  16659  isprm6  16768  phiprmpw  16830  pcneg  16929  prmpwdvds  16959  4sqlem19  17018  0ramcl  17078  imasleval  17590  catpropd  17760  funcres2c  17955  initoeu2  18068  oduprs  18351  latdisdlem  18547  acsfiindd  18604  dirtr  18653  chnind  18672  mndpsuppss  18818  mndind  18882  grpinveu  19036  mulgnn0subcl  19148  mulgsubcl  19149  mhmmulg  19176  cycsubm  19268  cycsubgcl  19272  cycsubgss  19273  ghmmulg  19293  odf1  19627  dfod2  19629  gexdvds2  19650  sylow2blem3  19687  frgpup1  19840  iscyggen2  19946  iscyg3  19951  prdsgsum  20046  ringrghm  20392  pwsgprod  20407  dvdsrcl2  20444  crngunit  20456  dvdsrpropd  20494  isdrng3lem2  20852  lss1d  21084  quscrng  21423  ssdifidllem  21484  ssdifidlprm  21486  mulgghm2  21626  frgpcyg  21723  ip0r  21787  isphld  21804  frlmgsum  21922  uvcresum  21943  psdmul  22329  coe1tmmul  22438  mdetdiagid  22757  cpmatmcllem  22875  tgcl  23126  0ntr  23228  innei  23282  neitr  23337  ordtrest2lem  23360  cncnp  23437  cnnei  23439  2ndcdisj  23613  dislly  23654  dissnlocfin  23686  kgenss  23700  ptcnplem  23778  ptcnp  23779  ptcn  23784  cnmpt2k  23845  qtoprest  23874  kqt0lem  23893  isr0  23894  kqreglem1  23898  trfilss  24046  isufil2  24065  ufileu  24076  hausflim  24138  cnextcn  24224  symgtgp  24263  tsmssubm  24300  tsmsxplem1  24310  ustfilxp  24370  ustuqtop0  24397  elbl2ps  24546  elbl2  24547  nrginvrcn  24849  nmoix  24886  nmoleub  24888  cncfco  25066  icccvx  25109  iscmet3  25452  rrxmet  25567  ovolfioo  25626  ovolficc  25627  ovolicc2lem4  25679  iunmbl2  25716  dyadmax  25757  mbfsup  25823  mbflimsup  25825  mbflim  25827  itg1addlem4  25858  mbfi1flimlem  25881  itg2monolem1  25909  itg2mono  25912  itg2i1fseqle  25913  itg2i1fseq  25914  itg2addlem  25917  itg2gt0  25919  itg2cnlem1  25920  itgfsum  25986  cnlimc  26047  dvlip2  26154  itgsubst  26208  plyeq0lem  26367  plypf1  26369  dvtaylp  26533  ulmcaulem  26557  ulmcau  26558  ulmcn  26562  ulmdvlem3  26565  mtest  26567  pserulm  26585  pserdvlem2  26591  logdivlt  26786  advlogexp  26820  cxpexp  26833  cxpcl  26839  xrlimcnp  27133  basellem4  27248  logexprlim  27389  dchrsum2  27432  sumdchr2  27434  rpvmasum2  27676  pntrsumbnd2  27731  pntleml  27775  noreson  27824  z12zsodd  28675  tglineeltr  28904  plngrotlem2  29070  brbtwn2  29255  colinearalglem4  29259  axeuclidlem  29312  axcontlem8  29321  axcontlem10  29323  grpoidinvlem3  30858  grpoideu  30861  grpoinveu  30871  nmcvcn  31047  nmounbi  31128  blocnilem  31156  ubthlem1  31222  h2hlm  31332  ocsh  31635  brafnmul  32303  kbpj  32308  nmcexi  32378  lnconi  32385  riesz1  32417  mdbr2  32648  mdsl0  32662  mdslmd3i  32684  csmdsymi  32686  atcvatlem  32737  chirredlem1  32742  chirredi  32746  cdj3lem2b  32789  xrge0infss  33105  mgcmntco  33314  lmodvslmhm  33370  suppgsumssiun  33392  gsumwrd2dccatlem  33397  submarchi  33506  dvdsruasso  33698  grplsm0l  33712  ssmxidllem  33756  rprmndvdsru  33819  r1plmhm  33899  mplvrpmmhm  33936  mplvrpmrhm  33937  esplyfval1  33963  lindsunlem  34014  lindsun  34015  fldextrspunlsplem  34063  extdgfialglem2  34083  madjusmdetlem2  34218  zarcmplem  34271  ordtrest2NEWlem  34312  voliune  34619  fsum2dsub  34994  circlemeth  35027  bnj110  35246  cvxsconn  35735  btwnouttr2  36514  cgrxfr  36547  btwnxfr  36548  lineext  36568  segcon2  36597  brsegle2  36601  seglecgr12im  36602  segletr  36606  broutsideof3  36618  outsideofeu  36623  lineunray  36639  lineelsb2  36640  nmulrid  36697  neibastop3  36873  ttcmin  37007  mh-inf3f1  37052  bj-imdiridlem  37829  isbasisrelowllem1  38001  isbasisrelowllem2  38002  fvineqsneu  38057  unccur  38254  fin2solem  38257  lindsadd  38264  matunitlindflem1  38267  matunitlindflem2  38268  poimirlem4  38275  poimirlem6  38277  poimirlem7  38278  poimirlem22  38293  poimirlem23  38294  poimirlem25  38296  poimirlem26  38297  poimirlem28  38299  poimirlem30  38301  poimirlem31  38302  poimirlem32  38303  poimir  38304  broucube  38305  heicant  38306  mblfinlem3  38310  volsupnfl  38316  itg2addnclem  38322  itg2addnclem2  38323  itg2addnclem3  38324  ftc1anclem1  38344  ftc1anclem5  38348  ftc1anclem6  38349  ftc1anc  38352  unirep  38365  filbcmb  38391  fzmul  38392  fdc  38396  nninfnub  38402  isbnd2  38434  bndss  38437  prdsbnd  38444  prdstotbnd  38445  ismtyres  38459  rrnmet  38480  rrncmslem  38483  rrnequiv  38486  ghomco  38542  grpokerinj  38544  rngonegmn1l  38592  isdrngo2  38609  rngoisocnv  38632  divrngidl  38679  intidl  38680  unichnidl  38682  prnc  38718  isfldidl  38719  cvrexchlem  40193  ps-2  40252  3atnelvolN  40360  dib1dim  41939  dib1dim2  41942  expeqidd  43086  evlselv  43321  fsuppind  43322  mzpindd  43477  dvdsabsmod0  43714  radcnvrat  45024  expgrowth  45045  modelac8prim  45701  fnchoice  45749  infxrbnd2  46084  infleinflem2  46086  xrralrecnnge  46105  limsuppnfdlem  46415  icccncfext  46601  dvnmul  46657  dvnprodlem2  46661  stoweidlem17  46731  stoweidlem30  46744  stoweidlem38  46752  stoweidlem42  46756  stoweidlem44  46758  fourierdlem31  46852  fourierdlem73  46893  fourierdlem74  46894  fourierdlem75  46895  fourierdlem83  46903  fourierdlem94  46914  fourierdlem113  46933  etransclem4  46952  hoicvr  47262  iinhoiicclem  47387  iccvonmbllem  47392  smfsuplem1  47525  smfsupdmmbllem  47558  smfinfdmmbllem  47562  itsclquadeu  49557  aacllem  50621