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

Theorem eqeq2 2150
Description: Equality implies equivalence of equalities. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
eqeq2 (𝐴 = 𝐵 → (𝐶 = 𝐴𝐶 = 𝐵))

Proof of Theorem eqeq2
StepHypRef Expression
1 eqeq1 2147 . 2 (𝐴 = 𝐵 → (𝐴 = 𝐶𝐵 = 𝐶))
2 eqcom 2142 . 2 (𝐶 = 𝐴𝐴 = 𝐶)
3 eqcom 2142 . 2 (𝐶 = 𝐵𝐵 = 𝐶)
41, 2, 33bitr4g 222 1 (𝐴 = 𝐵 → (𝐶 = 𝐴𝐶 = 𝐵))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 104   = 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-4 1488  ax-17 1507  ax-ext 2122
This theorem depends on definitions:  df-bi 116  df-cleq 2133
This theorem is referenced by:  eqeq2i  2151  eqeq2d  2152  eqeq12  2153  eleq1  2203  neeq2  2323  alexeq  2812  ceqex  2813  pm13.183  2823  eqeu  2855  mo2icl  2864  mob2  2865  euind  2872  reu6i  2876  reuind  2890  sbc5  2933  csbiebg  3043  sneq  3539  preqr1g  3697  preqr1  3699  prel12  3702  preq12bg  3704  opth  4163  euotd  4180  ordtriexmid  4441  wetriext  4495  tfisi  4505  ideqg  4694  resieq  4833  cnveqb  4998  cnveq0  4999  iota5  5112  funopg  5161  fneq2  5216  foeq3  5347  tz6.12f  5454  funbrfv  5464  fnbrfvb  5466  fvelimab  5481  elrnrexdm  5563  eufnfv  5652  f1veqaeq  5674  mpoeq123  5834  ovmpt4g  5897  ovi3  5911  ovg  5913  caovcang  5936  caovcan  5939  frecabcl  6300  nntri3or  6393  dcdifsnid  6404  nnaordex  6427  nnawordex  6428  ereq2  6441  eroveu  6524  2dom  6703  fundmen  6704  xpf1o  6742  nneneq  6755  tridc  6797  fisseneq  6824  fidcenumlemrks  6845  supsnti  6896  isotilem  6897  updjud  6971  nqtri3or  7224  ltexnqq  7236  aptisr  7607  srpospr  7611  map2psrprg  7633  axpre-apti  7713  nntopi  7722  subval  7974  eqord1  8265  divvalap  8454  nn0ind-raph  9188  frecuzrdgtcl  10212  frecuzrdgfunlem  10219  sqrtrval  10800  summodclem2  11179  prodmodclem2  11374  divides  11522  dvdstr  11557  odd2np1lem  11596  ndvdssub  11654  eucalglt  11765  hashgcdeq  11931  ennnfonelemim  11964  xmeteq0  12558  trilpo  13394  trirec0  13395  redcwlpo  13405
  Copyright terms: Public domain W3C validator