Theorem eqcomi 2119

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

Syntax hints:   = wceq 1314

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1406  ax-gen 1408  ax-ext 2097

This theorem depends on definitions:  df-bi 116  df-cleq 2108

This theorem is referenced by:  eqtr2i  2136  eqtr3i  2137  eqtr4i  2138  syl5eqr  2161  syl5reqr  2162  syl6eqr  2165  syl6reqr  2166  eqeltrri  2188  eleqtrri  2190  syl5eqelr  2202  syl6eleqr  2208  abid2  2235  abid2f  2280  eqnetrri  2307  neeqtrri  2311  eqsstrri  3096  sseqtr4i  3098  eqsstrrid  3110  syl6sseqr  3112  difdif2ss  3299  inrab2  3315  dfopg  3669  opid  3689  eqbrtrri  3916  breqtrri  3920  syl6breqr  3935  pwin  4164  limon  4389  tfis  4457  dfdm2  5031  cnvresid  5155  fores  5312  funcoeqres  5354  f1oprg  5365  fmptpr  5566  fsnunres  5576  riotaprop  5707  fo1st  6009  fo2nd  6010  fnmpoovd  6066  ixpsnf1o  6584  phplem4  6702  snnen2og  6706  phplem4on  6714  sbthlemi5  6801  eldju  6905  casefun  6922  omp1eomlem  6931  exmidfodomrlemim  7005  caucvgsrlembound  7536  ax0id  7613  1p1e2  8747  1e2m1  8749  2p1e3  8757  3p1e4  8759  4p1e5  8760  5p1e6  8761  6p1e7  8762  7p1e8  8763  8p1e9  8764  div4p1lem1div2  8877  0mnnnnn0  8913  zeo  9060  num0u  9096  numsucc  9125  decsucc  9126  1e0p1  9127  nummac  9130  decsubi  9148  decmul1  9149  decmul10add  9154  6p5lem  9155  10m1e9  9181  5t5e25  9188  6t6e36  9193  8t6e48  9204  decbin3  9227  infrenegsupex  9291  ige3m2fz  9722  fseq1p1m1  9767  fz0tp  9794  1fv  9809  fzo0to42pr  9890  fzosplitprm1  9904  expnegap0  10194  sq4e2t8  10283  3dec  10354  fihashen1  10438  pr0hash2ex  10454  imi  10565  infxrnegsupex  10924  zsumdc  11045  fsumadd  11067  hashrabrex  11142  efsep  11248  3dvdsdec  11410  3dvds2dec  11411  flodddiv4  11479  lcmneg  11601  ennnfonelem1  11765  ndxid  11826  2strstr1g  11905  toponrestid  12031  istpsi  12049  distopon  12099  distps  12103  discld  12148  txbas  12269  txdis  12288  txdis1cn  12289  ex-ceil  12631  ex-gcd  12636  bdceqir  12734  bj-ssom  12826  trilpolemgt1  12924