Theorem eqcomi 2085

Description: Inference from commutative law for class equality. (Contributed by NM, 5-Aug-1993.)

Hypothesis

Ref	Expression
eqcomi.1	⊢ 𝐴 = 𝐵

Assertion

Ref	Expression
eqcomi	⊢ 𝐵 = 𝐴

Proof of Theorem eqcomi

Step	Hyp	Ref	Expression
1		eqcomi.1	. 2 ⊢ 𝐴 = 𝐵
2		eqcom 2083	. 2 ⊢ (𝐴 = 𝐵 ↔ 𝐵 = 𝐴)
3	1, 2	mpbi 143	1 ⊢ 𝐵 = 𝐴

Syntax hints:   = 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:  eqtr2i  2102  eqtr3i  2103  eqtr4i  2104  syl5eqr  2127  syl5reqr  2128  syl6eqr  2131  syl6reqr  2132  eqeltrri  2152  eleqtrri  2154  syl5eqelr  2166  syl6eleqr  2172  abid2  2199  abid2f  2243  eqnetrri  2270  neeqtrri  2274  eqsstr3i  3030  sseqtr4i  3032  syl5eqssr  3044  syl6sseqr  3046  difdif2ss  3221  inrab2  3237  dfopg  3568  opid  3588  eqbrtrri  3806  breqtrri  3810  syl6breqr  3825  pwin  4037  limon  4257  tfis  4324  dfdm2  4872  cnvresid  4993  fores  5135  funcoeqres  5177  f1oprg  5188  fmptpr  5376  fsnunres  5385  riotaprop  5511  fo1st  5804  fo2nd  5805  phplem4  6341  snnen2og  6345  phplem4on  6353  caucvgsrlembound  6970  ax0id  7044  1p1e2  8155  1e2m1  8157  2p1e3  8165  3p1e4  8167  4p1e5  8168  5p1e6  8169  6p1e7  8170  7p1e8  8171  8p1e9  8172  div4p1lem1div2  8284  0mnnnnn0  8320  zeo  8452  num0u  8487  numsucc  8516  decsucc  8517  1e0p1  8518  nummac  8521  decsubi  8539  decmul1  8540  decmul10add  8545  6p5lem  8546  10m1e9  8572  5t5e25  8579  6t6e36  8584  8t6e48  8595  decbin3  8618  infrenegsupex  8682  ige3m2fz  9068  fseq1p1m1  9111  fz0tp  9135  1fv  9149  fzo0to42pr  9229  fzosplitprm1  9243  expnegap0  9484  3dec  9642  imi  9787  3dvdsdec  10264  3dvds2dec  10265  flodddiv4  10334  lcmneg  10456  ex-ceil  10564  ex-gcd  10568  bdceqir  10635  bj-ssom  10731