Theorem eqcomd 2088

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 2085	. 2 ⊢ (𝐴 = 𝐵 ↔ 𝐵 = 𝐴)
3	1, 2	sylib 120	1 ⊢ (𝜑 → 𝐵 = 𝐴)

Syntax hints:   → wi 4   = wceq 1285

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 1377  ax-gen 1379  ax-ext 2065

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

This theorem is referenced by:  eqtr2d  2116  eqtr3d  2117  eqtr4d  2118  syl5req  2128  syl6req  2132  sylan9req  2136  eqeltrrd  2160  eleqtrrd  2162  syl5eleqr  2172  syl6eqelr  2174  eqnetrrd  2275  neeqtrrd  2279  rspcedeq2vd  2720  dedhb  2772  eqsstr3d  3045  sseqtr4d  3047  syl6eqssr  3061  dfrab3ss  3260  uneqdifeqim  3349  ifbothdadc  3402  ifbothdc  3403  disjsn2  3479  diftpsn3  3552  dfopg  3594  unimax  3661  sndisj  3807  eqbrtrrd  3833  breqtrrd  3837  syl5breqr  3847  syl6eqbrr  3849  class2seteq  3963  opth1  4027  euotd  4045  opelopabsb  4051  tfisi  4365  0nelxp  4428  opeliunxp  4451  euiotaex  4950  iota4  4952  fun2ssres  5010  funimass1  5044  funssfv  5275  fnimapr  5309  fvun1  5315  fvco4  5321  fmptco  5406  foima2  5470  foeqcnvco  5509  f1eqcocnv  5510  f1oiso2  5545  riotass2  5573  riotass  5574  f1ocnvfv3  5580  caovlem2d  5772  f1opw2  5785  sbcopeq1a  5892  csbopeq1a  5893  eloprabi  5901  cnvf1olem  5924  f2ndf  5926  smoiso  5999  nnaword  6200  eqer  6254  uniqs  6280  mapsncnv  6382  ssenen  6497  findcard2  6535  findcard2s  6536  unsnfidcex  6557  fisseneq  6567  en1eqsn  6581  updjud  6680  fodjuomnilem0  6707  enq0sym  6894  enq0tr  6896  recexgt0sr  7222  caucvgsrlemoffcau  7246  axcaucvglemval  7335  le2tri3i  7496  cnegexlem2  7561  nnpcan  7608  addlsub  7751  negf1o  7763  subdi  7766  rereim  7963  cru  7979  divmulassap  8060  divmulasscomap  8061  divap1d  8165  div4p1lem1div2  8561  elz2  8714  zindd  8760  qapne  9019  divge1  9095  xrlttri3  9162  fseq1p1m1  9401  fzrevral  9412  nn0disj  9439  fzosplitsnm1  9509  fzosplitprm1  9534  flqlelt  9572  divfl0  9592  flqpmodeq  9623  zmodidfzo  9649  modqmuladd  9662  qnegmod  9665  addmodid  9668  modifeq2int  9682  modqeqmodmin  9690  modfzo0difsn  9691  modsumfzodifsn  9692  addmodlteq  9694  frecuzrdgsuc  9710  frecfzen2  9723  isersub  9779  expgt1  9830  leexp2r  9846  sqoddm1div8  9941  bcm1k  10003  bcn2m1  10012  hashinfuni  10020  hashennnuni  10022  hashennn  10023  hashunlem  10047  hashprg  10051  fihashssdif  10061  shftlem  10078  shftfvalg  10080  shftfval  10083  replim  10120  cjexp  10154  resqrexlemcalc1  10274  resqrexlemcvg  10279  rersqrtthlem  10290  abssq  10341  recan  10369  negfi  10484  climmpt  10513  climrecl  10536  fisumcvg  10574  summodnegmod  10607  dvdseq  10629  addmodlteqALT  10640  mulmoddvds  10644  zob  10671  nn0ob  10688  divalgmod  10707  flodddiv4  10714  divgcdnnr  10747  gcdneg  10753  bezoutlemsup  10778  dvdssq  10800  lcmneg  10836  3lcm2e6woprm  10848  6lcm4e12  10849  divgcdcoprmex  10864  cncongr1  10865  cncongrcoprm  10868  oddpwdclemxy  10927  oddpwdclemodd  10930  divnumden  10954  zgcdsq  10959  phibnd  10973  hashgcdlem  10983