ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  eqcomi GIF version

Theorem eqcomi 2060
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
StepHypRef Expression
1 eqcomi.1 . 2 𝐴 = 𝐵
2 eqcom 2058 . 2 (𝐴 = 𝐵𝐵 = 𝐴)
31, 2mpbi 137 1 𝐵 = 𝐴
Colors of variables: wff set class
Syntax hints:   = wceq 1259
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-5 1352  ax-gen 1354  ax-ext 2038
This theorem depends on definitions:  df-bi 114  df-cleq 2049
This theorem is referenced by:  eqtr2i  2077  eqtr3i  2078  eqtr4i  2079  syl5eqr  2102  syl5reqr  2103  syl6eqr  2106  syl6reqr  2107  eqeltrri  2127  eleqtrri  2129  syl5eqelr  2141  syl6eleqr  2147  abid2  2174  abid2f  2218  eqnetrri  2245  neeqtrri  2249  eqsstr3i  3003  sseqtr4i  3005  syl5eqssr  3017  syl6sseqr  3019  difdif2ss  3221  inrab2  3237  dfopg  3574  opid  3594  eqbrtrri  3812  breqtrri  3816  syl6breqr  3831  pwin  4046  limon  4266  tfis  4333  dfdm2  4879  cnvresid  5000  fores  5142  funcoeqres  5184  f1oprg  5195  fmptpr  5382  fsnunres  5391  riotaprop  5518  fo1st  5811  fo2nd  5812  phplem4  6348  snnen2og  6352  phplem4on  6359  caucvgsrlembound  6935  ax0id  7009  1p1e2  8105  1e2m1  8107  2p1e3  8115  3p1e4  8117  4p1e5  8118  5p1e6  8119  6p1e7  8120  7p1e8  8121  8p1e9  8122  div4p1lem1div2  8234  0mnnnnn0  8270  zeo  8401  num0u  8436  numsucc  8465  decsucc  8466  1e0p1  8467  nummac  8470  decsubi  8488  decmul1  8489  decmul10add  8494  6p5lem  8495  10m1e9  8521  5t5e25  8528  6t6e36  8533  8t6e48  8544  decbin3  8567  ige3m2fz  9014  fseq1p1m1  9057  fz0tp  9082  1fv  9097  fzo0to42pr  9177  fzosplitprm1  9191  expnegap0  9427  3dec  9585  imi  9727  3dvdsdec  10175  3dvds2dec  10176  ex-ceil  10259  bdceqir  10330  bj-ssom  10426
  Copyright terms: Public domain W3C validator