Theorem eqcomi 2089

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

Syntax hints:   = wceq 1287

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 1379  ax-gen 1381  ax-ext 2067

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

This theorem is referenced by:  eqtr2i  2106  eqtr3i  2107  eqtr4i  2108  syl5eqr  2131  syl5reqr  2132  syl6eqr  2135  syl6reqr  2136  eqeltrri  2158  eleqtrri  2160  syl5eqelr  2172  syl6eleqr  2178  abid2  2205  abid2f  2249  eqnetrri  2276  neeqtrri  2280  eqsstr3i  3046  sseqtr4i  3048  syl5eqssr  3060  syl6sseqr  3062  difdif2ss  3245  inrab2  3261  dfopg  3603  opid  3623  eqbrtrri  3841  breqtrri  3845  syl6breqr  3860  pwin  4082  limon  4302  tfis  4370  dfdm2  4928  cnvresid  5050  fores  5199  funcoeqres  5241  f1oprg  5252  fmptpr  5446  fsnunres  5455  riotaprop  5586  fo1st  5879  fo2nd  5880  phplem4  6517  snnen2og  6521  phplem4on  6529  sbthlemi5  6607  eldju  6696  casefun  6713  exmidfodomrlemim  6764  caucvgsrlembound  7276  ax0id  7350  1p1e2  8466  1e2m1  8468  2p1e3  8476  3p1e4  8478  4p1e5  8479  5p1e6  8480  6p1e7  8481  7p1e8  8482  8p1e9  8483  div4p1lem1div2  8595  0mnnnnn0  8631  zeo  8777  num0u  8812  numsucc  8841  decsucc  8842  1e0p1  8843  nummac  8846  decsubi  8864  decmul1  8865  decmul10add  8870  6p5lem  8871  10m1e9  8897  5t5e25  8904  6t6e36  8909  8t6e48  8920  decbin3  8943  infrenegsupex  9007  ige3m2fz  9388  fseq1p1m1  9431  fz0tp  9456  1fv  9471  fzo0to42pr  9552  fzosplitprm1  9566  expnegap0  9854  3dec  10012  fihashen1  10096  pr0hash2ex  10112  imi  10222  zisum  10656  3dvdsdec  10732  3dvds2dec  10733  flodddiv4  10801  lcmneg  10923  ex-ceil  11084  ex-gcd  11088  bdceqir  11165  bj-ssom  11261