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

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

Proof of Theorem eqeq2
StepHypRef Expression
1 eqeq1 2062 . 2 (𝐴 = 𝐵 → (𝐴 = 𝐶𝐵 = 𝐶))
2 eqcom 2058 . 2 (𝐶 = 𝐴𝐴 = 𝐶)
3 eqcom 2058 . 2 (𝐶 = 𝐵𝐵 = 𝐶)
41, 2, 33bitr4g 216 1 (𝐴 = 𝐵 → (𝐶 = 𝐴𝐶 = 𝐵))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 102   = 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-4 1416  ax-17 1435  ax-ext 2038
This theorem depends on definitions:  df-bi 114  df-cleq 2049
This theorem is referenced by:  eqeq2i  2066  eqeq2d  2067  eqeq12  2068  eleq1  2116  neeq2  2234  alexeq  2692  ceqex  2693  pm13.183  2703  eqeu  2733  mo2icl  2742  mob2  2743  euind  2750  reu6i  2754  reuind  2766  sbc5  2809  csbiebg  2916  sneq  3413  preqr1g  3564  preqr1  3566  prel12  3569  preq12bg  3571  opth  4001  euotd  4018  ordtriexmid  4274  wetriext  4328  tfisi  4337  ideqg  4514  resieq  4649  cnveqb  4803  cnveq0  4804  iota5  4914  funopg  4961  fneq2  5015  foeq3  5131  tz6.12f  5229  funbrfv  5239  fnbrfvb  5241  fvelimab  5256  elrnrexdm  5333  eufnfv  5416  f1veqaeq  5435  mpt2eq123  5591  ovmpt4g  5650  ovi3  5664  ovg  5666  caovcang  5689  caovcan  5692  nntri3or  6102  nnaordex  6130  nnawordex  6131  ereq2  6144  eroveu  6227  2dom  6315  fundmen  6316  nneneq  6350  supsnti  6408  isotilem  6409  nqtri3or  6551  ltexnqq  6563  aptisr  6920  srpospr  6924  axpre-apti  7016  nntopi  7025  subval  7265  divvalap  7726  nn0ind-raph  8413  frecuzrdgfn  9361  sqrtrval  9826  divides  10109  dvdstr  10143  odd2np1lem  10182
  Copyright terms: Public domain W3C validator