Theorem eqcomi 2144

Description: Inference from commutative law for class equality. (Contributed by NM, 5-Aug-1993.)

Hypothesis

Ref	Expression
eqcomi.1	|- A = B

Assertion

Ref	Expression
eqcomi	|- B = A

Proof of Theorem eqcomi

Step	Hyp	Ref	Expression
1		eqcomi.1	. 2 |- A = B
2		eqcom 2142	. 2 |- ( A = B <-> B = A )
3	1, 2	mpbi 144	1 |- B = A

Syntax hints:   = wceq 1332

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 1424  ax-gen 1426  ax-ext 2122

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

This theorem is referenced by:  eqtr2i  2162  eqtr3i  2163  eqtr4i  2164  syl5eqr  2187  syl5reqr  2188  eqtr4di  2191  eqtr4id  2192  eqeltrri  2214  eleqtrri  2216  eqeltrrid  2228  eleqtrrdi  2234  abid2  2261  abid2f  2307  eqnetrri  2334  neeqtrri  2338  eqsstrri  3135  sseqtrri  3137  eqsstrrid  3149  sseqtrrdi  3151  difdif2ss  3338  inrab2  3354  dfopg  3711  opid  3731  eqbrtrri  3959  breqtrri  3963  breqtrrdi  3978  pwin  4212  limon  4437  tfis  4505  dfdm2  5081  cnvresid  5205  fores  5362  funcoeqres  5406  f1oprg  5419  fmptpr  5620  fsnunres  5630  riotaprop  5761  fo1st  6063  fo2nd  6064  fnmpoovd  6120  ixpsnf1o  6638  phplem4  6757  snnen2og  6761  phplem4on  6769  sbthlemi5  6857  eldju  6961  casefun  6978  omp1eomlem  6987  exmidfodomrlemim  7074  caucvgsrlembound  7626  ax0id  7710  1p1e2  8861  1e2m1  8863  2p1e3  8877  3p1e4  8879  4p1e5  8880  5p1e6  8881  6p1e7  8882  7p1e8  8883  8p1e9  8884  div4p1lem1div2  8997  0mnnnnn0  9033  zeo  9180  num0u  9216  numsucc  9245  decsucc  9246  1e0p1  9247  nummac  9250  decsubi  9268  decmul1  9269  decmul10add  9274  6p5lem  9275  10m1e9  9301  5t5e25  9308  6t6e36  9313  8t6e48  9324  decbin3  9347  infrenegsupex  9416  ige3m2fz  9860  fseq1p1m1  9905  fz0tp  9932  1fv  9947  fzo0to42pr  10028  fzosplitprm1  10042  expnegap0  10332  sq4e2t8  10421  3dec  10492  fihashen1  10577  pr0hash2ex  10593  imi  10704  infxrnegsupex  11064  zsumdc  11185  fsumadd  11207  hashrabrex  11282  ntrivcvgap  11349  efsep  11434  3dvdsdec  11598  3dvds2dec  11599  flodddiv4  11667  lcmneg  11791  ennnfonelem1  11956  ndxid  12022  2strstr1g  12101  toponrestid  12227  istpsi  12245  distopon  12295  distps  12299  discld  12344  txbas  12466  txdis  12485  txdis1cn  12486  txhmeo  12527  txswaphmeolem  12528  dvexp  12883  sinq34lt0t  12960  loge  12996  2logb9irr  13096  2logb9irrALT  13099  sqrt2cxp2logb9e3  13100  2logb9irrap  13102  ex-ceil  13109  ex-gcd  13114  bdceqir  13213  bj-ssom  13305  trilpolemgt1  13407  redcwlpolemeq1  13421