Theorem eqcomd 2090

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

Step	Hyp	Ref	Expression
1		eqcomd.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		eqcom 2087	. 2 ⊢ (𝐴 = 𝐵 ↔ 𝐵 = 𝐴)
3	1, 2	sylib 120	1 ⊢ (𝜑 → 𝐵 = 𝐴)

Syntax hints:   → wi 4   = wceq 1287

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1379  ax-gen 1381  ax-ext 2067

This theorem depends on definitions:  df-bi 115  df-cleq 2078

This theorem is referenced by:  eqtr2d  2118  eqtr3d  2119  eqtr4d  2120  syl5req  2130  syl6req  2134  sylan9req  2138  eqeltrrd  2162  eleqtrrd  2164  syl5eleqr  2174  syl6eqelr  2176  eqnetrrd  2277  neeqtrrd  2281  rspcedeq2vd  2723  dedhb  2775  eqsstr3d  3050  sseqtr4d  3052  syl6eqssr  3066  dfrab3ss  3266  uneqdifeqim  3355  ifbothdadc  3408  ifbothdc  3409  disjsn2  3490  diftpsn3  3563  dfopg  3605  unimax  3672  sndisj  3818  eqbrtrrd  3844  breqtrrd  3848  syl5breqr  3858  syl6eqbrr  3860  class2seteq  3975  opth1  4039  euotd  4057  opelopabsb  4063  tfisi  4377  0nelxp  4440  opeliunxp  4463  euiotaex  4964  iota4  4966  fun2ssres  5024  funimass1  5058  funssfv  5295  fnimapr  5329  fvun1  5335  fvco4  5341  fmptco  5429  foima2  5493  foeqcnvco  5532  f1eqcocnv  5533  f1oiso2  5569  riotass2  5597  riotass  5598  f1ocnvfv3  5604  caovlem2d  5796  f1opw2  5809  sbcopeq1a  5916  csbopeq1a  5917  eloprabi  5925  cnvf1olem  5948  f2ndf  5950  smoiso  6023  nnaword  6224  eqer  6278  uniqs  6304  mapsncnv  6406  ssenen  6521  findcard2  6559  findcard2s  6560  unsnfidcex  6584  fisseneq  6595  en1eqsn  6609  sbthlemi6  6618  updjud  6720  fodjuomnilem0  6749  enq0sym  6938  enq0tr  6940  recexgt0sr  7266  caucvgsrlemoffcau  7290  axcaucvglemval  7379  le2tri3i  7540  cnegexlem2  7605  nnpcan  7652  addlsub  7795  negf1o  7807  subdi  7810  rereim  8007  cru  8023  divmulassap  8104  divmulasscomap  8105  divap1d  8209  div4p1lem1div2  8605  elz2  8754  zindd  8800  qapne  9059  divge1  9135  xrlttri3  9202  fseq1p1m1  9441  fzrevral  9452  nn0disj  9480  fzosplitsnm1  9551  fzosplitprm1  9576  flqlelt  9614  divfl0  9634  flqpmodeq  9665  zmodidfzo  9691  modqmuladd  9704  qnegmod  9707  addmodid  9710  modifeq2int  9724  modqeqmodmin  9732  modfzo0difsn  9733  modsumfzodifsn  9734  addmodlteq  9736  frecuzrdgsuc  9752  frecfzen2  9765  iseqf1olemab  9826  iseqf1olemmo  9829  isersub  9843  expgt1  9895  leexp2r  9911  sqoddm1div8  10006  bcm1k  10068  bcn2m1  10077  hashinfuni  10085  hashennnuni  10087  hashennn  10088  hashunlem  10112  hashprg  10116  fihashssdif  10126  zfz1isolem1  10145  shftlem  10150  shftfvalg  10152  shftfval  10155  replim  10192  cjexp  10226  resqrexlemcalc1  10346  resqrexlemcvg  10351  rersqrtthlem  10362  abssq  10413  recan  10441  negfi  10557  climmpt  10586  climrecl  10609  fisumcvg  10661  isummolem3  10664  isummolem2a  10665  summodnegmod  10733  dvdseq  10755  addmodlteqALT  10766  mulmoddvds  10770  zob  10797  nn0ob  10814  divalgmod  10833  flodddiv4  10840  divgcdnnr  10873  gcdneg  10879  bezoutlemsup  10904  dvdssq  10926  lcmneg  10962  3lcm2e6woprm  10974  6lcm4e12  10975  divgcdcoprmex  10990  cncongr1  10991  cncongrcoprm  10994  oddpwdclemxy  11053  oddpwdclemodd  11056  divnumden  11080  zgcdsq  11085  phibnd  11099  hashgcdlem  11109