Theorem eqcomd 2176

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

Syntax hints:   → wi 4   = wceq 1348

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 1440  ax-gen 1442  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-cleq 2163

This theorem is referenced by:  eqtr2d  2204  eqtr3d  2205  eqtr4d  2206  eqtr2id  2216  eqtr2di  2220  sylan9req  2224  eqeltrrd  2248  eleqtrrd  2250  eleqtrrid  2260  eqeltrrdi  2262  eqnetrrd  2366  neeqtrrd  2370  rspcedeq2vd  2844  dedhb  2899  eqsstrrd  3184  sseqtrrd  3186  eqsstrrdi  3200  dfrab3ss  3405  uneqdifeqim  3500  ifbothdadc  3557  ifbothdc  3558  disjsn2  3646  diftpsn3  3721  dfopg  3763  unimax  3830  sndisj  3985  eqbrtrrd  4013  breqtrrd  4017  breqtrrid  4027  eqbrtrrdi  4029  class2seteq  4149  opth1  4221  euotd  4239  opelopabsb  4245  tfisi  4571  0nelxp  4639  opeliunxp  4666  euiotaex  5176  iota4  5178  iotam  5190  fun2ssres  5241  funimass1  5275  funssfv  5522  fnimapr  5556  fvun1  5562  fvco4  5568  elfvmptrab  5591  fmptco  5662  foima2  5731  foeqcnvco  5769  f1eqcocnv  5770  f1oiso2  5806  riotass2  5835  riotass  5836  f1ocnvfv3  5842  caovlem2d  6045  f1opw2  6055  sbcopeq1a  6166  csbopeq1a  6167  eloprabi  6175  cnvf1olem  6203  f2ndf  6205  smoiso  6281  nnaword  6490  eqer  6545  uniqs  6571  mapsncnv  6673  ixpiinm  6702  mapsnf1o  6715  ssenen  6829  findcard2  6867  findcard2s  6868  unsnfidcex  6897  fisseneq  6909  phpeqd  6910  en1eqsn  6925  sbthlemi6  6939  updjud  7059  omp1eomlem  7071  nnnninf2  7103  nninfisollem0  7106  nninfisollemeq  7108  fodju0  7123  3nsssucpw1  7213  enq0sym  7394  enq0tr  7396  recexgt0sr  7735  caucvgsrlemoffcau  7760  axcaucvglemval  7859  le2tri3i  8028  cnegexlem2  8095  nnpcan  8142  addlsub  8289  negf1o  8301  subdi  8304  rereim  8505  cru  8521  divmulassap  8612  divmulasscomap  8613  divap1d  8718  div4p1lem1div2  9131  difgtsumgt  9281  elz2  9283  zindd  9330  qapne  9598  divge1  9680  xrlttri3  9754  fseq1p1m1  10050  fzrevral  10061  nn0disj  10094  fzosplitsnm1  10165  fzosplitprm1  10190  flqlelt  10232  divfl0  10252  flqpmodeq  10283  zmodidfzo  10309  modqmuladd  10322  qnegmod  10325  addmodid  10328  modifeq2int  10342  modqeqmodmin  10350  modfzo0difsn  10351  modsumfzodifsn  10352  addmodlteq  10354  frecuzrdgsuc  10370  frecfzen2  10383  iseqf1olemab  10445  iseqf1olemmo  10448  ser3sub  10462  expgt1  10514  leexp2r  10530  sqoddm1div8  10629  bcm1k  10694  bcn2m1  10703  hashinfuni  10711  hashennnuni  10713  hashennn  10714  hashunlem  10739  hashprg  10743  fihashssdif  10753  zfz1isolem1  10775  shftlem  10780  shftfvalg  10782  shftfval  10785  replim  10823  cjexp  10857  resqrexlemcalc1  10978  resqrexlemcvg  10983  rersqrtthlem  10994  abssq  11045  recan  11073  negfi  11191  minclpr  11200  mingeb  11205  xrmaxiflemcom  11212  xrmineqinf  11232  xrminltinf  11235  xrminadd  11238  climmpt  11263  climrecl  11287  fsum3cvg  11341  summodclem3  11343  summodclem2a  11344  modfsummodlemstep  11420  isumsplit  11454  arisum  11461  geosergap  11469  geo2sum  11477  mertenslemi1  11498  mertenslem2  11499  clim2divap  11503  fproddccvg  11535  fprodssdc  11553  fprodabs  11579  fproddivapf  11594  fprodmodd  11604  efcj  11636  efsub  11644  eflegeo  11664  sinneg  11689  cosneg  11690  sin01bnd  11720  cos01bnd  11721  modm1div  11762  summodnegmod  11784  dvdseq  11808  addmodlteqALT  11819  mulmoddvds  11823  zob  11850  nn0ob  11867  divalgmod  11886  flodddiv4  11893  divgcdnnr  11931  gcdneg  11937  bezoutlemsup  11964  dvdssq  11986  lcmneg  12028  3lcm2e6woprm  12040  6lcm4e12  12041  divgcdcoprmex  12056  cncongr1  12057  cncongrcoprm  12060  oddpwdclemxy  12123  oddpwdclemodd  12126  divnumden  12150  zgcdsq  12155  phibnd  12171  hashgcdlem  12192  vfermltl  12205  powm2modprm  12206  reumodprminv  12207  pythagtriplem19  12236  pcprendvds2  12245  pczpre  12251  dvdsprmpweqle  12290  difsqpwdvds  12291  4sqlem4  12344  ennnfonelemex  12369  strndxid  12444  topnvalg  12591  intopsn  12621  ismgmid2  12634  mgmidsssn0  12638  mndpfo  12674  mndfo  12675  mndinvmod  12678  mnd1id  12680  mhmf1o  12693  0mhm  12704  grpidd2  12744  grpinvid2  12755  toponcom  12819  tgtopon  12860  restopnb  12975  cnptoprest  13033  blfvalps  13179  bdmopn  13298  cnmet  13324  limcdifap  13425  dviaddf  13463  dvexp  13469  coseq0negpitopi  13551  abssinper  13561  rplogbzexp  13666  lgsvalmod  13714  lgsneg  13719  subctctexmid  14034  cvgcmp2nlemabs  14064  trilpolemlt1  14073