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

Theorem eqcomi 2086
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 2084 . 2  |-  ( A  =  B  <->  B  =  A )
31, 2mpbi 143 1  |-  B  =  A
Colors of variables: wff set class
Syntax hints:    = wceq 1285
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 1377  ax-gen 1379  ax-ext 2064
This theorem depends on definitions:  df-bi 115  df-cleq 2075
This theorem is referenced by:  eqtr2i  2103  eqtr3i  2104  eqtr4i  2105  syl5eqr  2128  syl5reqr  2129  syl6eqr  2132  syl6reqr  2133  eqeltrri  2153  eleqtrri  2155  syl5eqelr  2167  syl6eleqr  2173  abid2  2200  abid2f  2244  eqnetrri  2271  neeqtrri  2275  eqsstr3i  3031  sseqtr4i  3033  syl5eqssr  3045  syl6sseqr  3047  difdif2ss  3228  inrab2  3244  dfopg  3576  opid  3596  eqbrtrri  3814  breqtrri  3818  syl6breqr  3833  pwin  4045  limon  4265  tfis  4332  dfdm2  4882  cnvresid  5004  fores  5146  funcoeqres  5188  f1oprg  5199  fmptpr  5387  fsnunres  5396  riotaprop  5522  fo1st  5815  fo2nd  5816  phplem4  6390  snnen2og  6394  phplem4on  6402  caucvgsrlembound  7032  ax0id  7106  1p1e2  8222  1e2m1  8224  2p1e3  8232  3p1e4  8234  4p1e5  8235  5p1e6  8236  6p1e7  8237  7p1e8  8238  8p1e9  8239  div4p1lem1div2  8351  0mnnnnn0  8387  zeo  8533  num0u  8568  numsucc  8597  decsucc  8598  1e0p1  8599  nummac  8602  decsubi  8620  decmul1  8621  decmul10add  8626  6p5lem  8627  10m1e9  8653  5t5e25  8660  6t6e36  8665  8t6e48  8676  decbin3  8699  infrenegsupex  8763  ige3m2fz  9144  fseq1p1m1  9187  fz0tp  9212  1fv  9226  fzo0to42pr  9306  fzosplitprm1  9320  expnegap0  9581  3dec  9739  sizeen1  9823  pr0size2ex  9839  imi  9925  3dvdsdec  10409  3dvds2dec  10410  flodddiv4  10478  lcmneg  10600  ex-ceil  10715  ex-gcd  10719  bdceqir  10793  bj-ssom  10889
  Copyright terms: Public domain W3C validator