Theorem eqcomd 2086

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 2083	. 2 |- ( A = B <-> B = A )
3	1, 2	sylib 120	1 |- ( ph -> B = A )

Syntax hints:   -> wi 4   = wceq 1284

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 1376  ax-gen 1378  ax-ext 2063

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

This theorem is referenced by:  eqtr2d  2114  eqtr3d  2115  eqtr4d  2116  syl5req  2126  syl6req  2130  sylan9req  2134  eqeltrrd  2156  eleqtrrd  2158  syl5eleqr  2168  syl6eqelr  2170  eqnetrrd  2271  neeqtrrd  2275  rspcedeq2vd  2710  dedhb  2761  eqsstr3d  3034  sseqtr4d  3036  syl6eqssr  3050  dfrab3ss  3242  uneqdifeqim  3328  ifbothdc  3380  disjsn2  3455  diftpsn3  3527  dfopg  3568  unimax  3635  sndisj  3781  eqbrtrrd  3807  breqtrrd  3811  syl5breqr  3821  syl6eqbrr  3823  class2seteq  3937  opth1  3991  euotd  4009  opelopabsb  4015  tfisi  4328  0nelxp  4390  opeliunxp  4413  euiotaex  4903  iota4  4905  fun2ssres  4963  funimass1  4996  funssfv  5220  fnimapr  5254  fvun1  5260  fmptco  5351  foeqcnvco  5450  f1eqcocnv  5451  f1oiso2  5486  riotass2  5514  riotass  5515  f1ocnvfv3  5521  caovlem2d  5713  f1opw2  5726  sbcopeq1a  5833  csbopeq1a  5834  eloprabi  5842  cnvf1olem  5865  f2ndf  5867  smoiso  5940  nnaword  6107  eqer  6161  uniqs  6187  findcard2  6373  findcard2s  6374  unsnfidcex  6385  enq0sym  6622  enq0tr  6624  recexgt0sr  6950  caucvgsrlemoffcau  6974  axcaucvglemval  7063  le2tri3i  7219  cnegexlem2  7284  nnpcan  7331  addlsub  7474  negf1o  7486  subdi  7489  rereim  7686  cru  7702  divmulassap  7783  divmulasscomap  7784  divap1d  7888  div4p1lem1div2  8284  elz2  8419  zindd  8465  qapne  8724  divge1  8800  xrlttri3  8872  fseq1p1m1  9111  fzrevral  9122  nn0disj  9148  fzosplitsnm1  9218  fzosplitprm1  9243  flqlelt  9278  divfl0  9298  flqpmodeq  9329  zmodidfzo  9355  modqmuladd  9368  qnegmod  9371  addmodid  9374  modifeq2int  9388  modqeqmodmin  9396  modfzo0difsn  9397  modsumfzodifsn  9398  addmodlteq  9400  frecuzrdgsuc  9417  frecfzen2  9420  isersub  9464  expgt1  9514  leexp2r  9530  sqoddm1div8  9625  bcm1k  9687  bcn2m1  9696  shftlem  9704  shftfvalg  9706  shftfval  9709  replim  9746  cjexp  9780  resqrexlemcalc1  9900  resqrexlemcvg  9905  rersqrtthlem  9916  abssq  9967  recan  9995  negfi  10110  climmpt  10139  climrecl  10162  summodnegmod  10226  dvdseq  10248  addmodlteqALT  10259  mulmoddvds  10263  zob  10291  nn0ob  10308  divalgmod  10327  flodddiv4  10334  divgcdnnr  10367  gcdneg  10373  bezoutlemsup  10398  dvdssq  10420  lcmneg  10456  3lcm2e6woprm  10468  6lcm4e12  10469  divgcdcoprmex  10484  cncongr1  10485  cncongrcoprm  10488  oddpwdclemxy  10547  oddpwdclemodd  10550