Theorem eqcomd 2193

Description: Deduction from commutative law for class equality. (Contributed by NM, 15-Aug-1994.)

Hypothesis

Ref	Expression
eqcomd.1	|- ( ph -> A = B )

Assertion

Ref	Expression
eqcomd	|- ( ph -> B = A )

Proof of Theorem eqcomd

Step	Hyp	Ref	Expression
1		eqcomd.1	. 2 |- ( ph -> A = B )
2		eqcom 2189	. 2 |- ( A = B <-> B = A )
3	1, 2	sylib 122	1 |- ( ph -> B = A )

Syntax hints:   -> wi 4   = wceq 1363

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 1457  ax-gen 1459  ax-ext 2169

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

This theorem is referenced by:  eqtr2d  2221  eqtr3d  2222  eqtr4d  2223  eqtr2id  2233  eqtr2di  2237  sylan9req  2241  eqeltrrd  2265  eleqtrrd  2267  eleqtrrid  2277  eqeltrrdi  2279  eqnetrrd  2383  neeqtrrd  2387  rspcedeq2vd  2863  dedhb  2918  eqsstrrd  3204  sseqtrrd  3206  eqsstrrdi  3220  dfrab3ss  3425  uneqdifeqim  3520  ifbothdadc  3578  ifbothdc  3579  disjsn2  3667  diftpsn3  3745  dfopg  3788  unimax  3855  sndisj  4011  eqbrtrrd  4039  breqtrrd  4043  breqtrrid  4053  eqbrtrrdi  4055  class2seteq  4175  opth1  4248  euotd  4266  opelopabsb  4272  tfisi  4598  0nelxp  4666  opeliunxp  4693  euiotaex  5206  iota4  5208  iotam  5220  fun2ssres  5271  funimass1  5305  funssfv  5553  fnimapr  5589  fvun1  5595  fvco4  5601  elfvmptrab  5624  fmptco  5695  foima2  5765  foeqcnvco  5804  f1eqcocnv  5805  f1oiso2  5841  riotass2  5870  riotass  5871  f1ocnvfv3  5877  caovlem2d  6081  f1opw2  6091  sbcopeq1a  6202  csbopeq1a  6203  eloprabi  6211  cnvf1olem  6239  f2ndf  6241  smoiso  6317  nnaword  6526  eqer  6581  uniqs  6607  mapsncnv  6709  ixpiinm  6738  mapsnf1o  6751  ssenen  6865  findcard2  6903  findcard2s  6904  unsnfidcex  6933  fisseneq  6945  phpeqd  6946  en1eqsn  6961  sbthlemi6  6975  updjud  7095  omp1eomlem  7107  nnnninf2  7139  nninfisollem0  7142  nninfisollemeq  7144  fodju0  7159  3nsssucpw1  7249  enq0sym  7445  enq0tr  7447  recexgt0sr  7786  caucvgsrlemoffcau  7811  axcaucvglemval  7910  le2tri3i  8080  cnegexlem2  8147  nnpcan  8194  addlsub  8341  negf1o  8353  subdi  8356  rereim  8557  cru  8573  divmulassap  8666  divmulasscomap  8667  divap1d  8772  div4p1lem1div2  9186  difgtsumgt  9336  elz2  9338  zindd  9385  qapne  9653  divge1  9737  xrlttri3  9811  fseq1p1m1  10108  fzrevral  10119  nn0disj  10152  fzosplitsnm1  10223  fzosplitprm1  10248  flqlelt  10290  divfl0  10310  flqpmodeq  10341  zmodidfzo  10367  modqmuladd  10380  qnegmod  10383  addmodid  10386  modifeq2int  10400  modqeqmodmin  10408  modfzo0difsn  10409  modsumfzodifsn  10410  addmodlteq  10412  frecuzrdgsuc  10428  frecfzen2  10441  iseqf1olemab  10503  iseqf1olemmo  10506  ser3sub  10520  expgt1  10572  leexp2r  10588  sqoddm1div8  10688  mulsubdivbinom2ap  10705  bcm1k  10754  bcn2m1  10763  hashinfuni  10771  hashennnuni  10773  hashennn  10774  hashunlem  10798  hashprg  10802  fihashssdif  10812  zfz1isolem1  10834  shftlem  10839  shftfvalg  10841  shftfval  10844  replim  10882  cjexp  10916  resqrexlemcalc1  11037  resqrexlemcvg  11042  rersqrtthlem  11053  abssq  11104  recan  11132  negfi  11250  minclpr  11259  mingeb  11264  xrmaxiflemcom  11271  xrmineqinf  11291  xrminltinf  11294  xrminadd  11297  climmpt  11322  climrecl  11346  fsum3cvg  11400  summodclem3  11402  summodclem2a  11403  modfsummodlemstep  11479  isumsplit  11513  arisum  11520  geosergap  11528  geo2sum  11536  mertenslemi1  11557  mertenslem2  11558  clim2divap  11562  fproddccvg  11594  fprodssdc  11612  fprodabs  11638  fproddivapf  11653  fprodmodd  11663  efcj  11695  efsub  11703  eflegeo  11723  sinneg  11748  cosneg  11749  sin01bnd  11779  cos01bnd  11780  modm1div  11821  summodnegmod  11843  dvdseq  11868  addmodlteqALT  11879  mulmoddvds  11883  zob  11910  nn0ob  11927  divalgmod  11946  flodddiv4  11953  divgcdnnr  11991  gcdneg  11997  bezoutlemsup  12024  dvdssq  12046  lcmneg  12088  3lcm2e6woprm  12100  6lcm4e12  12101  divgcdcoprmex  12116  cncongr1  12117  cncongrcoprm  12120  oddpwdclemxy  12183  oddpwdclemodd  12186  divnumden  12210  zgcdsq  12215  phibnd  12231  hashgcdlem  12252  vfermltl  12265  powm2modprm  12266  reumodprminv  12267  pythagtriplem19  12296  pcprendvds2  12305  pczpre  12311  dvdsprmpweqle  12350  difsqpwdvds  12351  4sqlem4  12404  ennnfonelemex  12429  strndxid  12504  topnvalg  12718  intopsn  12805  ismgmid2  12818  mgmidsssn0  12822  mndpfo  12861  mndfo  12862  mndinvmod  12868  mnd1id  12870  mhmf1o  12883  0mhm  12895  grpidd2  12938  grpinvid2  12950  grpidssd  12973  grpnpcan  12989  grpsubsub4  12990  qusgrp2  13008  mulginvcom  13040  grpissubg  13086  imasabl  13171  mgpress  13183  rnglz  13197  rngrz  13198  rngmneg1  13199  rngmneg2  13200  rngpropd  13207  srg1zr  13239  srgmulgass  13241  srgpcomp  13242  srgpcomppsc  13244  ringadd2  13279  ringo2times  13280  ringlz  13295  ringrz  13296  ringinvnzdiv  13300  ringnegl  13301  ringnegr  13302  imasring  13312  qusring2  13314  crngunit  13359  lringuplu  13416  lmod0vs  13510  lmodvsmmulgdi  13512  lmodfopne  13515  islss3  13568  lspsn  13605  lmodindp1  13617  rnglidlmmgm  13685  rnglidlmsgrp  13686  rnglidlrng  13687  isridl  13692  zringinvg  13776  toponcom  13823  tgtopon  13862  restopnb  13977  cnptoprest  14035  blfvalps  14181  bdmopn  14300  cnmet  14326  limcdifap  14427  dviaddf  14465  dvexp  14471  coseq0negpitopi  14553  abssinper  14563  rplogbzexp  14668  lgsvalmod  14716  lgsneg  14721  subctctexmid  15047  cvgcmp2nlemabs  15077  trilpolemlt1  15086