Theorem eqcomi 2087

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 2085	. 2 ⊢ (𝐴 = 𝐵 ↔ 𝐵 = 𝐴)
3	1, 2	mpbi 143	1 ⊢ 𝐵 = 𝐴

Syntax hints:   = wceq 1285

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 1377  ax-gen 1379  ax-ext 2065

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

This theorem is referenced by:  eqtr2i  2104  eqtr3i  2105  eqtr4i  2106  syl5eqr  2129  syl5reqr  2130  syl6eqr  2133  syl6reqr  2134  eqeltrri  2156  eleqtrri  2158  syl5eqelr  2170  syl6eleqr  2176  abid2  2203  abid2f  2247  eqnetrri  2274  neeqtrri  2278  eqsstr3i  3041  sseqtr4i  3043  syl5eqssr  3055  syl6sseqr  3057  difdif2ss  3239  inrab2  3255  dfopg  3594  opid  3614  eqbrtrri  3832  breqtrri  3836  syl6breqr  3851  pwin  4073  limon  4293  tfis  4361  dfdm2  4919  cnvresid  5041  fores  5190  funcoeqres  5232  f1oprg  5243  fmptpr  5431  fsnunres  5440  riotaprop  5570  fo1st  5863  fo2nd  5864  phplem4  6501  snnen2og  6505  phplem4on  6513  eldju  6666  casefun  6683  exmidfodomrlemim  6730  caucvgsrlembound  7242  ax0id  7316  1p1e2  8432  1e2m1  8434  2p1e3  8442  3p1e4  8444  4p1e5  8445  5p1e6  8446  6p1e7  8447  7p1e8  8448  8p1e9  8449  div4p1lem1div2  8561  0mnnnnn0  8597  zeo  8747  num0u  8782  numsucc  8811  decsucc  8812  1e0p1  8813  nummac  8816  decsubi  8834  decmul1  8835  decmul10add  8840  6p5lem  8841  10m1e9  8867  5t5e25  8874  6t6e36  8879  8t6e48  8890  decbin3  8913  infrenegsupex  8977  ige3m2fz  9358  fseq1p1m1  9401  fz0tp  9426  1fv  9440  fzo0to42pr  9520  fzosplitprm1  9534  expnegap0  9800  3dec  9958  fihashen1  10042  pr0hash2ex  10058  imi  10161  3dvdsdec  10645  3dvds2dec  10646  flodddiv4  10714  lcmneg  10836  ex-ceil  10997  ex-gcd  11001  bdceqir  11078  bj-ssom  11174