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

Theorem eqcomd 2183
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 2179 . 2 (𝐴 = 𝐵𝐵 = 𝐴)
31, 2sylib 122 1 (𝜑𝐵 = 𝐴)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1353
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1447  ax-gen 1449  ax-ext 2159
This theorem depends on definitions:  df-bi 117  df-cleq 2170
This theorem is referenced by:  eqtr2d  2211  eqtr3d  2212  eqtr4d  2213  eqtr2id  2223  eqtr2di  2227  sylan9req  2231  eqeltrrd  2255  eleqtrrd  2257  eleqtrrid  2267  eqeltrrdi  2269  eqnetrrd  2373  neeqtrrd  2377  rspcedeq2vd  2851  dedhb  2906  eqsstrrd  3192  sseqtrrd  3194  eqsstrrdi  3208  dfrab3ss  3413  uneqdifeqim  3508  ifbothdadc  3565  ifbothdc  3566  disjsn2  3654  diftpsn3  3732  dfopg  3774  unimax  3841  sndisj  3996  eqbrtrrd  4024  breqtrrd  4028  breqtrrid  4038  eqbrtrrdi  4040  class2seteq  4160  opth1  4233  euotd  4251  opelopabsb  4257  tfisi  4583  0nelxp  4651  opeliunxp  4678  euiotaex  5190  iota4  5192  iotam  5204  fun2ssres  5255  funimass1  5289  funssfv  5537  fnimapr  5572  fvun1  5578  fvco4  5584  elfvmptrab  5607  fmptco  5678  foima2  5747  foeqcnvco  5785  f1eqcocnv  5786  f1oiso2  5822  riotass2  5851  riotass  5852  f1ocnvfv3  5858  caovlem2d  6061  f1opw2  6071  sbcopeq1a  6182  csbopeq1a  6183  eloprabi  6191  cnvf1olem  6219  f2ndf  6221  smoiso  6297  nnaword  6506  eqer  6561  uniqs  6587  mapsncnv  6689  ixpiinm  6718  mapsnf1o  6731  ssenen  6845  findcard2  6883  findcard2s  6884  unsnfidcex  6913  fisseneq  6925  phpeqd  6926  en1eqsn  6941  sbthlemi6  6955  updjud  7075  omp1eomlem  7087  nnnninf2  7119  nninfisollem0  7122  nninfisollemeq  7124  fodju0  7139  3nsssucpw1  7229  enq0sym  7422  enq0tr  7424  recexgt0sr  7763  caucvgsrlemoffcau  7788  axcaucvglemval  7887  le2tri3i  8056  cnegexlem2  8123  nnpcan  8170  addlsub  8317  negf1o  8329  subdi  8332  rereim  8533  cru  8549  divmulassap  8641  divmulasscomap  8642  divap1d  8747  div4p1lem1div2  9161  difgtsumgt  9311  elz2  9313  zindd  9360  qapne  9628  divge1  9710  xrlttri3  9784  fseq1p1m1  10080  fzrevral  10091  nn0disj  10124  fzosplitsnm1  10195  fzosplitprm1  10220  flqlelt  10262  divfl0  10282  flqpmodeq  10313  zmodidfzo  10339  modqmuladd  10352  qnegmod  10355  addmodid  10358  modifeq2int  10372  modqeqmodmin  10380  modfzo0difsn  10381  modsumfzodifsn  10382  addmodlteq  10384  frecuzrdgsuc  10400  frecfzen2  10413  iseqf1olemab  10475  iseqf1olemmo  10478  ser3sub  10492  expgt1  10544  leexp2r  10560  sqoddm1div8  10659  bcm1k  10724  bcn2m1  10733  hashinfuni  10741  hashennnuni  10743  hashennn  10744  hashunlem  10768  hashprg  10772  fihashssdif  10782  zfz1isolem1  10804  shftlem  10809  shftfvalg  10811  shftfval  10814  replim  10852  cjexp  10886  resqrexlemcalc1  11007  resqrexlemcvg  11012  rersqrtthlem  11023  abssq  11074  recan  11102  negfi  11220  minclpr  11229  mingeb  11234  xrmaxiflemcom  11241  xrmineqinf  11261  xrminltinf  11264  xrminadd  11267  climmpt  11292  climrecl  11316  fsum3cvg  11370  summodclem3  11372  summodclem2a  11373  modfsummodlemstep  11449  isumsplit  11483  arisum  11490  geosergap  11498  geo2sum  11506  mertenslemi1  11527  mertenslem2  11528  clim2divap  11532  fproddccvg  11564  fprodssdc  11582  fprodabs  11608  fproddivapf  11623  fprodmodd  11633  efcj  11665  efsub  11673  eflegeo  11693  sinneg  11718  cosneg  11719  sin01bnd  11749  cos01bnd  11750  modm1div  11791  summodnegmod  11813  dvdseq  11837  addmodlteqALT  11848  mulmoddvds  11852  zob  11879  nn0ob  11896  divalgmod  11915  flodddiv4  11922  divgcdnnr  11960  gcdneg  11966  bezoutlemsup  11993  dvdssq  12015  lcmneg  12057  3lcm2e6woprm  12069  6lcm4e12  12070  divgcdcoprmex  12085  cncongr1  12086  cncongrcoprm  12089  oddpwdclemxy  12152  oddpwdclemodd  12155  divnumden  12179  zgcdsq  12184  phibnd  12200  hashgcdlem  12221  vfermltl  12234  powm2modprm  12235  reumodprminv  12236  pythagtriplem19  12265  pcprendvds2  12274  pczpre  12280  dvdsprmpweqle  12319  difsqpwdvds  12320  4sqlem4  12373  ennnfonelemex  12398  strndxid  12473  topnvalg  12648  intopsn  12678  ismgmid2  12691  mgmidsssn0  12695  mndpfo  12731  mndfo  12732  mndinvmod  12736  mnd1id  12738  mhmf1o  12751  0mhm  12763  grpidd2  12804  grpinvid2  12815  grpidssd  12835  grpnpcan  12851  grpsubsub4  12852  mulginvcom  12896  srg1zr  12996  srgmulgass  12998  srgpcomp  12999  srgpcomppsc  13001  ringadd2  13036  rngo2times  13037  ringlz  13048  ringrz  13049  ringinvnzdiv  13053  ringnegl  13054  rngnegr  13055  crngunit  13105  toponcom  13192  tgtopon  13233  restopnb  13348  cnptoprest  13406  blfvalps  13552  bdmopn  13671  cnmet  13697  limcdifap  13798  dviaddf  13836  dvexp  13842  coseq0negpitopi  13924  abssinper  13934  rplogbzexp  14039  lgsvalmod  14087  lgsneg  14092  subctctexmid  14406  cvgcmp2nlemabs  14436  trilpolemlt1  14445
  Copyright terms: Public domain W3C validator