Theorem eqcomi 2168

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

Syntax hints:   = wceq 1342

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 1434  ax-gen 1436  ax-ext 2146

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

This theorem is referenced by:  eqtr2i  2186  eqtr3i  2187  eqtr4i  2188  eqtr3id  2211  eqtr3di  2212  eqtr4di  2215  eqtr4id  2216  eqeltrri  2238  eleqtrri  2240  eqeltrrid  2252  eleqtrrdi  2258  abid2  2285  abid2f  2332  eqnetrri  2359  neeqtrri  2363  eqsstrri  3170  sseqtrri  3172  eqsstrrid  3184  sseqtrrdi  3186  difdif2ss  3374  inrab2  3390  dfopg  3750  opid  3770  eqbrtrri  3999  breqtrri  4003  breqtrrdi  4018  pwin  4254  limon  4484  tfis  4554  dfdm2  5132  cnvresid  5256  fores  5413  funcoeqres  5457  f1oprg  5470  fmptpr  5671  fsnunres  5681  riotaprop  5815  fo1st  6117  fo2nd  6118  fnmpoovd  6174  ixpsnf1o  6693  phplem4  6812  snnen2og  6816  phplem4on  6824  pw1dc0el  6868  ss1o0el1o  6869  sbthlemi5  6917  eldju  7024  casefun  7041  omp1eomlem  7050  exmidfodomrlemim  7148  caucvgsrlembound  7726  ax0id  7810  1p1e2  8965  1e2m1  8967  2p1e3  8981  3p1e4  8983  4p1e5  8984  5p1e6  8985  6p1e7  8986  7p1e8  8987  8p1e9  8988  div4p1lem1div2  9101  0mnnnnn0  9137  zeo  9287  num0u  9323  numsucc  9352  decsucc  9353  1e0p1  9354  nummac  9357  decsubi  9375  decmul1  9376  decmul10add  9381  6p5lem  9382  10m1e9  9408  5t5e25  9415  6t6e36  9420  8t6e48  9431  decbin3  9454  infrenegsupex  9523  ige3m2fz  9974  fseq1p1m1  10019  fz0tp  10047  fz0to4untppr  10049  1fv  10064  fzo0to42pr  10145  fzosplitprm1  10159  expnegap0  10453  sq4e2t8  10542  3dec  10616  fihashen1  10701  pr0hash2ex  10717  imi  10828  infxrnegsupex  11190  zsumdc  11311  fsumadd  11333  hashrabrex  11408  ntrivcvgap  11475  fprodmul  11518  fproddivapf  11558  fprodmodd  11568  efsep  11618  3dvdsdec  11787  3dvds2dec  11788  flodddiv4  11856  lcmneg  11985  ennnfonelem1  12277  nninfdclemp1  12322  ndxid  12355  2strstr1g  12434  toponrestid  12560  istpsi  12578  distopon  12628  distps  12632  discld  12677  txbas  12799  txdis  12818  txdis1cn  12819  txhmeo  12860  txswaphmeolem  12861  dvexp  13216  sinq34lt0t  13293  loge  13329  2logb9irr  13430  2logb9irrALT  13433  sqrt2cxp2logb9e3  13434  2logb9irrap  13436  ex-ceil  13444  ex-gcd  13449  bj-charfundcALT  13526  bdceqir  13561  bj-ssom  13653  trilpolemgt1  13752  redcwlpolemeq1  13767