Theorem eqcomd 2236

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

Syntax hints:   → wi 4   = wceq 1397

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 1495  ax-gen 1497  ax-ext 2212

This theorem depends on definitions:  df-bi 117  df-cleq 2223

This theorem is referenced by:  eqtr2d  2264  eqtr3d  2265  eqtr4d  2266  eqtr2id  2276  eqtr2di  2280  sylan9req  2284  eqeltrrd  2308  eleqtrrd  2310  eleqtrrid  2320  eqeltrrdi  2322  eqnetrrd  2427  neeqtrrd  2431  rspcedeq2vd  2919  dedhb  2974  eqsstrrd  3263  sseqtrrd  3265  eqsstrrdi  3279  dfrab3ss  3484  uneqdifeqim  3579  ifbothdadc  3640  ifbothdc  3641  2if2dc  3646  disjsn2  3733  diftpsn3  3815  elpr2elpr  3860  dfopg  3861  unimax  3928  sndisj  4085  eqbrtrrd  4113  breqtrrd  4117  breqtrrid  4127  eqbrtrrdi  4129  class2seteq  4255  opth1  4330  euotd  4349  opelopabsb  4356  tfisi  4687  0nelxp  4755  opeliunxp  4783  euiotaex  5305  iota4  5308  iotam  5320  fun2ssres  5372  funimass1  5409  funssfv  5668  fnimapr  5709  fvun1  5715  fvco4  5721  elfvmptrab  5745  fmptco  5816  fncofn  5835  foima2  5897  foeqcnvco  5936  f1eqcocnv  5937  f1oiso2  5973  riotass2  6005  riotass  6006  f1ocnvfv3  6012  fvmpopr2d  6163  caovlem2d  6220  f1opw2  6234  offveq  6261  sbcopeq1a  6355  csbopeq1a  6356  eloprabi  6366  cnvf1olem  6394  f2ndf  6396  smoiso  6473  nnaword  6684  eqer  6739  uniqs  6767  mapsncnv  6869  ixpiinm  6898  mapsnf1o  6911  ssenen  7042  findcard2  7083  findcard2s  7084  unsnfidcex  7117  fisseneq  7132  phpeqd  7133  en1eqsn  7152  sbthlemi6  7166  updjud  7286  omp1eomlem  7298  nnnninf2  7331  nninfisollem0  7334  nninfisollemeq  7336  fodju0  7351  3nsssucpw1  7459  enq0sym  7657  enq0tr  7659  recexgt0sr  7998  caucvgsrlemoffcau  8023  axcaucvglemval  8122  le2tri3i  8293  cnegexlem2  8360  nnpcan  8407  addlsub  8554  negf1o  8566  subdi  8569  rereim  8771  cru  8787  divmulassap  8880  divmulasscomap  8881  divap1d  8986  subhalfhalf  9384  div4p1lem1div2  9403  difgtsumgt  9554  elz2  9556  zindd  9603  qapne  9878  divge1  9963  xrlttri3  10037  fseq1p1m1  10334  fzrevral  10345  nn0disj  10378  fzo0addel  10439  fzosplitsnm1  10460  fzosplitprm1  10486  flqlelt  10542  divfl0  10562  flqpmodeq  10595  zmodidfzo  10621  modqmuladd  10634  qnegmod  10637  addmodid  10640  modifeq2int  10654  modqeqmodmin  10662  modfzo0difsn  10663  modsumfzodifsn  10664  addmodlteq  10666  frecuzrdgsuc  10682  frecfzen2  10695  iseqf1olemab  10770  iseqf1olemmo  10773  seqf1oglem1  10787  seqf1oglem2  10788  ser3sub  10791  expgt1  10845  leexp2r  10861  sqoddm1div8  10961  mulsubdivbinom2ap  10979  bcm1k  11028  bcn2m1  11037  hashinfuni  11045  hashennnuni  11047  hashennn  11048  hashunlem  11073  hashprg  11078  fihashssdif  11088  zfz1isolem1  11110  elovmpowrd  11164  ccatsymb  11188  ccatlid  11192  eqs1  11214  ccatw2s1p1g  11231  swrdfv2  11253  swrds1  11258  swrdlsw  11259  pfxfv  11274  swrdswrd  11295  swrdpfx  11297  pfxpfx  11298  pfxlswccat  11303  ccats1pfxeq  11304  wrdind  11312  wrd2ind  11313  pfxccatin12lem1  11318  pfxccatin12lem2  11321  swrdccat3blem  11329  swrdccat3b  11330  ccats1pfxeqbi  11332  reuccatpfxs1lem  11336  reuccatpfxs1  11337  s3s4d  11393  s2s5d  11394  s5s2d  11395  shftlem  11399  shftfvalg  11401  shftfval  11404  replim  11442  cjexp  11476  resqrexlemcalc1  11597  resqrexlemcvg  11602  rersqrtthlem  11613  abssq  11664  recan  11692  negfi  11811  minclpr  11820  mingeb  11825  xrmaxiflemcom  11832  xrmineqinf  11852  xrminltinf  11855  xrminadd  11858  climmpt  11883  climrecl  11907  fsum3cvg  11962  summodclem3  11964  summodclem2a  11965  modfsummodlemstep  12041  isumsplit  12075  arisum  12082  geosergap  12090  geo2sum  12098  mertenslemi1  12119  mertenslem2  12120  clim2divap  12124  fproddccvg  12156  fprodssdc  12174  fprodabs  12200  fproddivapf  12215  fprodmodd  12225  efcj  12257  efsub  12265  eflegeo  12285  sinneg  12310  cosneg  12311  sin01bnd  12341  cos01bnd  12342  modm1div  12384  summodnegmod  12406  dvdseq  12432  addmodlteqALT  12443  mulmoddvds  12447  zob  12475  nn0ob  12492  divalgmod  12511  flodddiv4  12520  bitsinv1  12546  divgcdnnr  12570  gcdneg  12576  bezoutlemsup  12603  dvdssq  12625  lcmneg  12669  3lcm2e6woprm  12681  6lcm4e12  12682  divgcdcoprmex  12697  cncongr1  12698  cncongrcoprm  12701  oddpwdclemxy  12764  oddpwdclemodd  12767  divnumden  12791  zgcdsq  12796  phibnd  12812  hashgcdlem  12833  vfermltl  12847  powm2modprm  12848  reumodprminv  12849  pythagtriplem19  12878  pcprendvds2  12887  pczpre  12893  dvdsprmpweqle  12933  difsqpwdvds  12934  4sqlem4  12988  ennnfonelemex  13058  strndxid  13133  topnvalg  13357  prdssca  13381  intopsn  13473  ismgmid2  13486  mgmidsssn0  13490  gsumfzval  13497  gsumprval  13505  mndpfo  13544  mndfo  13545  mndinvmod  13551  prds0g  13555  mnd1id  13562  mhmf1o  13576  0mhm  13592  gsumwmhm  13604  grpidd2  13647  grpinvid2  13659  grpidssd  13682  grpnpcan  13698  grpsubsub4  13699  qusgrp2  13723  mulginvcom  13757  grpissubg  13804  quselbasg  13840  qus0  13845  ecqusaddd  13848  ghmid  13859  ghminv  13860  imasabl  13946  gsumfzmhm  13953  gsumsplit0  13956  mgpress  13968  rnglz  13982  rngrz  13983  rngmneg1  13984  rngmneg2  13985  rngpropd  13992  srg1zr  14024  srgmulgass  14026  srgpcomp  14027  srgpcomppsc  14029  ringadd2  14064  ringo2times  14065  ringlz  14080  ringrz  14081  ringinvnzdiv  14087  ringnegl  14088  ringnegr  14089  imasring  14101  qusring2  14103  crngunit  14149  rhmopp  14214  lringuplu  14234  opprdomnbg  14312  lmod0vs  14359  lmodvsmmulgdi  14361  lmodfopne  14364  islss3  14417  lspsn  14454  lmodindp1  14466  rnglidlmmgm  14534  rnglidlmsgrp  14535  rnglidlrng  14536  isridl  14542  zringinvg  14642  zndvds  14687  znf1o  14689  psrgrp  14728  toponcom  14780  tgtopon  14819  restopnb  14934  cnptoprest  14992  blfvalps  15138  bdmopn  15257  cnmet  15283  mpomulcn  15319  limcdifap  15415  dvidsslem  15446  dviaddf  15458  dvexp  15464  dvply2g  15519  coseq0negpitopi  15589  abssinper  15599  rplogbzexp  15707  dvdsppwf1o  15742  mpodvdsmulf1o  15743  fsumdvdsmul  15744  sgmmul  15749  perfect  15754  lgsvalmod  15777  lgsneg  15782  gausslemma2dlem1a  15816  gausslemma2dlem6  15825  gausslemma2dlem7  15826  gausslemma2d  15827  lgsquadlem2  15836  2lgslem1a1  15844  2lgslem1a  15846  2lgslem3c  15853  2lgslem3d  15854  2lgslem3d1  15858  2lgs  15862  2lgsoddprm  15871  uhgrun  15966  upgrun  16006  umgrun  16008  ushgredgedg  16106  issubgr2  16138  uhgrissubgr  16141  subgruhgredgdm  16150  subumgredg2en  16151  subupgr  16153  p1evtxdeqfilem  16191  wlklenvm1  16221  wlklenvm1g  16222  wlkl1loop  16238  upgriswlkdc  16240  uspgr2wlkeq  16245  uspgr2wlkeq2  16246  uspgr2wlkeqi  16247  wlkres  16259  loopclwwlkn1b  16299  clwwlkn1loopb  16300  clwwlkext2edg  16302  clwwlknonccat  16313  s2elclwwlknon2  16316  clwwlknonex2lem2  16318  clwwlknun  16321  eupth2lem3fi  16356  eupth2lembfi  16357  subctctexmid  16661  cvgcmp2nlemabs  16703  trilpolemlt1  16712  gsumgfsumlem  16751  gfsumsn  16753