Theorem eqcomd 2045

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

Syntax hints:   → wi 4   = wceq 1243

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-gen 1338  ax-ext 2022

This theorem depends on definitions:  df-bi 110  df-cleq 2033

This theorem is referenced by:  eqtr2d  2073  eqtr3d  2074  eqtr4d  2075  syl5req  2085  syl6req  2089  sylan9req  2093  eqeltrrd  2115  eleqtrrd  2117  syl5eleqr  2127  syl6eqelr  2129  eqnetrrd  2231  neeqtrrd  2235  dedhb  2710  eqsstr3d  2980  sseqtr4d  2982  syl6eqssr  2996  dfrab3ss  3215  uneqdifeqim  3308  ifbothdc  3357  disjsn2  3433  diftpsn3  3505  dfopg  3547  unimax  3614  sndisj  3760  eqbrtrrd  3786  breqtrrd  3790  syl5breqr  3800  syl6eqbrr  3802  class2seteq  3916  opth1  3973  euotd  3991  opelopabsb  3997  tfisi  4310  0nelxp  4372  opeliunxp  4395  euiotaex  4883  iota4  4885  fun2ssres  4943  funimass1  4976  funssfv  5199  fnimapr  5233  fvun1  5239  fmptco  5330  foeqcnvco  5430  f1eqcocnv  5431  f1oiso2  5466  riotass2  5494  riotass  5495  f1ocnvfv3  5501  caovlem2d  5693  f1opw2  5706  sbcopeq1a  5813  csbopeq1a  5814  eloprabi  5822  cnvf1olem  5845  f2ndf  5847  smoiso  5917  nnaword  6084  eqer  6138  uniqs  6164  findcard2  6346  findcard2s  6347  enq0sym  6530  enq0tr  6532  recexgt0sr  6858  caucvgsrlemoffcau  6882  axcaucvglemval  6971  le2tri3i  7126  cnegexlem2  7187  nnpcan  7234  subdi  7382  rereim  7577  cru  7593  divap1d  7776  div4p1lem1div2  8177  elz2  8312  zindd  8356  qapne  8574  divge1  8649  xrlttri3  8718  fseq1p1m1  8956  fzrevral  8967  nn0disj  8995  fzosplitsnm1  9065  fzosplitprm1  9090  flqlelt  9118  divfl0  9138  flqpmodeq  9169  frecuzrdgsuc  9201  frecfzen2  9204  isersub  9244  expgt1  9293  leexp2r  9308  shftlem  9417  shftfvalg  9419  shftfval  9422  replim  9459  cjexp  9493  resqrexlemcalc1  9612  resqrexlemcvg  9617  rersqrtthlem  9628  abssq  9677  recan  9705  climmpt  9821  climrecl  9844