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

Theorem eqcomi 2089
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
StepHypRef Expression
1 eqcomi.1 . 2  |-  A  =  B
2 eqcom 2087 . 2  |-  ( A  =  B  <->  B  =  A )
31, 2mpbi 143 1  |-  B  =  A
Colors of variables: wff set class
Syntax hints:    = wceq 1287
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1379  ax-gen 1381  ax-ext 2067
This theorem depends on definitions:  df-bi 115  df-cleq 2078
This theorem is referenced by:  eqtr2i  2106  eqtr3i  2107  eqtr4i  2108  syl5eqr  2131  syl5reqr  2132  syl6eqr  2135  syl6reqr  2136  eqeltrri  2158  eleqtrri  2160  syl5eqelr  2172  syl6eleqr  2178  abid2  2205  abid2f  2249  eqnetrri  2276  neeqtrri  2280  eqsstr3i  3046  sseqtr4i  3048  syl5eqssr  3060  syl6sseqr  3062  difdif2ss  3245  inrab2  3261  dfopg  3603  opid  3623  eqbrtrri  3841  breqtrri  3845  syl6breqr  3860  pwin  4083  limon  4303  tfis  4371  dfdm2  4931  cnvresid  5053  fores  5205  funcoeqres  5247  f1oprg  5258  fmptpr  5452  fsnunres  5461  riotaprop  5592  fo1st  5885  fo2nd  5886  phplem4  6523  snnen2og  6527  phplem4on  6535  sbthlemi5  6614  eldju  6703  casefun  6720  exmidfodomrlemim  6771  caucvgsrlembound  7283  ax0id  7357  1p1e2  8473  1e2m1  8475  2p1e3  8483  3p1e4  8485  4p1e5  8486  5p1e6  8487  6p1e7  8488  7p1e8  8489  8p1e9  8490  div4p1lem1div2  8602  0mnnnnn0  8638  zeo  8784  num0u  8819  numsucc  8848  decsucc  8849  1e0p1  8850  nummac  8853  decsubi  8871  decmul1  8872  decmul10add  8877  6p5lem  8878  10m1e9  8904  5t5e25  8911  6t6e36  8916  8t6e48  8927  decbin3  8950  infrenegsupex  9014  ige3m2fz  9395  fseq1p1m1  9438  fz0tp  9463  1fv  9478  fzo0to42pr  9559  fzosplitprm1  9573  expnegap0  9862  3dec  10020  fihashen1  10104  pr0hash2ex  10120  imi  10230  zisum  10665  3dvdsdec  10747  3dvds2dec  10748  flodddiv4  10816  lcmneg  10938  ex-ceil  11099  ex-gcd  11103  bdceqir  11180  bj-ssom  11276
  Copyright terms: Public domain W3C validator