Theorem eqcomi 2169

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

Syntax hints:   = wceq 1343

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1435  ax-gen 1437  ax-ext 2147

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

This theorem is referenced by:  eqtr2i  2187  eqtr3i  2188  eqtr4i  2189  eqtr3id  2213  eqtr3di  2214  eqtr4di  2217  eqtr4id  2218  eqeltrri  2240  eleqtrri  2242  eqeltrrid  2254  eleqtrrdi  2260  abid2  2287  abid2f  2334  eqnetrri  2361  neeqtrri  2365  eqsstrri  3175  sseqtrri  3177  eqsstrrid  3189  sseqtrrdi  3191  difdif2ss  3379  inrab2  3395  dfopg  3756  opid  3776  eqbrtrri  4005  breqtrri  4009  breqtrrdi  4024  pwin  4260  limon  4490  tfis  4560  dfdm2  5138  cnvresid  5262  fores  5419  funcoeqres  5463  f1oprg  5476  fmptpr  5677  fsnunres  5687  riotaprop  5821  fo1st  6125  fo2nd  6126  fnmpoovd  6183  ixpsnf1o  6702  phplem4  6821  snnen2og  6825  phplem4on  6833  pw1dc0el  6877  ss1o0el1o  6878  sbthlemi5  6926  eldju  7033  casefun  7050  omp1eomlem  7059  exmidfodomrlemim  7157  caucvgsrlembound  7735  ax0id  7819  1p1e2  8974  1e2m1  8976  2p1e3  8990  3p1e4  8992  4p1e5  8993  5p1e6  8994  6p1e7  8995  7p1e8  8996  8p1e9  8997  div4p1lem1div2  9110  0mnnnnn0  9146  zeo  9296  num0u  9332  numsucc  9361  decsucc  9362  1e0p1  9363  nummac  9366  decsubi  9384  decmul1  9385  decmul10add  9390  6p5lem  9391  10m1e9  9417  5t5e25  9424  6t6e36  9429  8t6e48  9440  decbin3  9463  infrenegsupex  9532  ige3m2fz  9984  fseq1p1m1  10029  fz0tp  10057  fz0to4untppr  10059  1fv  10074  fzo0to42pr  10155  fzosplitprm1  10169  expnegap0  10463  sq4e2t8  10552  3dec  10627  fihashen1  10712  pr0hash2ex  10728  imi  10842  infxrnegsupex  11204  zsumdc  11325  fsumadd  11347  hashrabrex  11422  ntrivcvgap  11489  fprodmul  11532  fproddivapf  11572  fprodmodd  11582  efsep  11632  3dvdsdec  11802  3dvds2dec  11803  flodddiv4  11871  lcmneg  12006  ennnfonelem1  12340  nninfdclemp1  12383  ndxid  12418  2strstr1g  12498  toponrestid  12659  istpsi  12677  distopon  12727  distps  12731  discld  12776  txbas  12898  txdis  12917  txdis1cn  12918  txhmeo  12959  txswaphmeolem  12960  dvexp  13315  sinq34lt0t  13392  loge  13428  2logb9irr  13529  2logb9irrALT  13532  sqrt2cxp2logb9e3  13533  2logb9irrap  13535  lgsdir  13576  2sqlem9  13600  2sqlem10  13601  ex-ceil  13607  ex-gcd  13612  bj-charfundcALT  13691  bdceqir  13726  bj-ssom  13818  trilpolemgt1  13918  redcwlpolemeq1  13933