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

Theorem eqcomi 2143
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 2141 . 2  |-  ( A  =  B  <->  B  =  A )
31, 2mpbi 144 1  |-  B  =  A
Colors of variables: wff set class
Syntax hints:    = wceq 1331
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 1423  ax-gen 1425  ax-ext 2121
This theorem depends on definitions:  df-bi 116  df-cleq 2132
This theorem is referenced by:  eqtr2i  2161  eqtr3i  2162  eqtr4i  2163  syl5eqr  2186  syl5reqr  2187  syl6eqr  2190  syl6reqr  2191  eqeltrri  2213  eleqtrri  2215  eqeltrrid  2227  eleqtrrdi  2233  abid2  2260  abid2f  2306  eqnetrri  2333  neeqtrri  2337  eqsstrri  3130  sseqtrri  3132  eqsstrrid  3144  sseqtrrdi  3146  difdif2ss  3333  inrab2  3349  dfopg  3703  opid  3723  eqbrtrri  3951  breqtrri  3955  breqtrrdi  3970  pwin  4204  limon  4429  tfis  4497  dfdm2  5073  cnvresid  5197  fores  5354  funcoeqres  5398  f1oprg  5411  fmptpr  5612  fsnunres  5622  riotaprop  5753  fo1st  6055  fo2nd  6056  fnmpoovd  6112  ixpsnf1o  6630  phplem4  6749  snnen2og  6753  phplem4on  6761  sbthlemi5  6849  eldju  6953  casefun  6970  omp1eomlem  6979  exmidfodomrlemim  7062  caucvgsrlembound  7614  ax0id  7698  1p1e2  8849  1e2m1  8851  2p1e3  8865  3p1e4  8867  4p1e5  8868  5p1e6  8869  6p1e7  8870  7p1e8  8871  8p1e9  8872  div4p1lem1div2  8985  0mnnnnn0  9021  zeo  9168  num0u  9204  numsucc  9233  decsucc  9234  1e0p1  9235  nummac  9238  decsubi  9256  decmul1  9257  decmul10add  9262  6p5lem  9263  10m1e9  9289  5t5e25  9296  6t6e36  9301  8t6e48  9312  decbin3  9335  infrenegsupex  9401  ige3m2fz  9841  fseq1p1m1  9886  fz0tp  9913  1fv  9928  fzo0to42pr  10009  fzosplitprm1  10023  expnegap0  10313  sq4e2t8  10402  3dec  10473  fihashen1  10557  pr0hash2ex  10573  imi  10684  infxrnegsupex  11044  zsumdc  11165  fsumadd  11187  hashrabrex  11262  ntrivcvgap  11329  efsep  11409  3dvdsdec  11573  3dvds2dec  11574  flodddiv4  11642  lcmneg  11766  ennnfonelem1  11931  ndxid  11997  2strstr1g  12076  toponrestid  12202  istpsi  12220  distopon  12270  distps  12274  discld  12319  txbas  12441  txdis  12460  txdis1cn  12461  txhmeo  12502  txswaphmeolem  12503  dvexp  12858  sinq34lt0t  12934  loge  12968  ex-ceil  12997  ex-gcd  13002  bdceqir  13101  bj-ssom  13193  trilpolemgt1  13293
  Copyright terms: Public domain W3C validator