ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  eqcomd GIF version

Theorem eqcomd 2121
Description: Deduction from commutative law for class equality. (Contributed by NM, 15-Aug-1994.)
Hypothesis
Ref Expression
eqcomd.1 (𝜑𝐴 = 𝐵)
Assertion
Ref Expression
eqcomd (𝜑𝐵 = 𝐴)

Proof of Theorem eqcomd
StepHypRef Expression
1 eqcomd.1 . 2 (𝜑𝐴 = 𝐵)
2 eqcom 2117 . 2 (𝐴 = 𝐵𝐵 = 𝐴)
31, 2sylib 121 1 (𝜑𝐵 = 𝐴)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1314
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1406  ax-gen 1408  ax-ext 2097
This theorem depends on definitions:  df-bi 116  df-cleq 2108
This theorem is referenced by:  eqtr2d  2149  eqtr3d  2150  eqtr4d  2151  syl5req  2161  syl6req  2165  sylan9req  2169  eqeltrrd  2193  eleqtrrd  2195  eleqtrrid  2205  syl6eqelr  2207  eqnetrrd  2309  neeqtrrd  2313  rspcedeq2vd  2771  dedhb  2824  eqsstrrd  3102  sseqtrrd  3104  eqsstrrdi  3118  dfrab3ss  3322  uneqdifeqim  3416  ifbothdadc  3471  ifbothdc  3472  disjsn2  3554  diftpsn3  3629  dfopg  3671  unimax  3738  sndisj  3893  eqbrtrrd  3920  breqtrrd  3924  breqtrrid  3934  eqbrtrrdi  3936  class2seteq  4055  opth1  4126  euotd  4144  opelopabsb  4150  tfisi  4469  0nelxp  4535  opeliunxp  4562  euiotaex  5072  iota4  5074  fun2ssres  5134  funimass1  5168  funssfv  5413  fnimapr  5447  fvun1  5453  fvco4  5459  elfvmptrab  5482  fmptco  5552  foima2  5619  foeqcnvco  5657  f1eqcocnv  5658  f1oiso2  5694  riotass2  5722  riotass  5723  f1ocnvfv3  5729  caovlem2d  5929  f1opw2  5942  sbcopeq1a  6051  csbopeq1a  6052  eloprabi  6060  cnvf1olem  6087  f2ndf  6089  smoiso  6165  nnaword  6373  eqer  6427  uniqs  6453  mapsncnv  6555  ixpiinm  6584  mapsnf1o  6597  ssenen  6711  findcard2  6749  findcard2s  6750  unsnfidcex  6774  fisseneq  6786  phpeqd  6787  en1eqsn  6802  sbthlemi6  6816  updjud  6933  omp1eomlem  6945  fodju0  6985  enq0sym  7204  enq0tr  7206  recexgt0sr  7545  caucvgsrlemoffcau  7570  axcaucvglemval  7669  le2tri3i  7836  cnegexlem2  7902  nnpcan  7949  addlsub  8096  negf1o  8108  subdi  8111  rereim  8311  cru  8327  divmulassap  8418  divmulasscomap  8419  divap1d  8524  div4p1lem1div2  8927  elz2  9076  zindd  9123  qapne  9383  divge1  9461  xrlttri3  9534  fseq1p1m1  9825  fzrevral  9836  nn0disj  9866  fzosplitsnm1  9937  fzosplitprm1  9962  flqlelt  10000  divfl0  10020  flqpmodeq  10051  zmodidfzo  10077  modqmuladd  10090  qnegmod  10093  addmodid  10096  modifeq2int  10110  modqeqmodmin  10118  modfzo0difsn  10119  modsumfzodifsn  10120  addmodlteq  10122  frecuzrdgsuc  10138  frecfzen2  10151  iseqf1olemab  10213  iseqf1olemmo  10216  ser3sub  10230  expgt1  10282  leexp2r  10298  sqoddm1div8  10395  bcm1k  10457  bcn2m1  10466  hashinfuni  10474  hashennnuni  10476  hashennn  10477  hashunlem  10501  hashprg  10505  fihashssdif  10515  zfz1isolem1  10534  shftlem  10539  shftfvalg  10541  shftfval  10544  replim  10582  cjexp  10616  resqrexlemcalc1  10737  resqrexlemcvg  10742  rersqrtthlem  10753  abssq  10804  recan  10832  negfi  10950  minclpr  10959  xrmaxiflemcom  10969  xrmineqinf  10989  xrminltinf  10992  xrminadd  10995  climmpt  11020  climrecl  11044  fsum3cvg  11097  summodclem3  11100  summodclem2a  11101  modfsummodlemstep  11177  isumsplit  11211  arisum  11218  geosergap  11226  geo2sum  11234  mertenslemi1  11255  mertenslem2  11256  efcj  11289  efsub  11297  eflegeo  11318  sinneg  11343  cosneg  11344  sin01bnd  11374  cos01bnd  11375  summodnegmod  11431  dvdseq  11453  addmodlteqALT  11464  mulmoddvds  11468  zob  11495  nn0ob  11512  divalgmod  11531  flodddiv4  11538  divgcdnnr  11571  gcdneg  11577  bezoutlemsup  11604  dvdssq  11626  lcmneg  11662  3lcm2e6woprm  11674  6lcm4e12  11675  divgcdcoprmex  11690  cncongr1  11691  cncongrcoprm  11694  oddpwdclemxy  11753  oddpwdclemodd  11756  divnumden  11780  zgcdsq  11785  phibnd  11799  hashgcdlem  11809  ennnfonelemex  11833  strndxid  11893  topnvalg  12038  toponcom  12100  tgtopon  12141  restopnb  12256  cnptoprest  12314  blfvalps  12460  bdmopn  12579  cnmet  12605  limcdifap  12706  dviaddf  12744  dvexp  12750  subctctexmid  13030  cvgcmp2nlemabs  13061  trilpolemlt1  13068
  Copyright terms: Public domain W3C validator