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

Theorem eqeq2 2065
Description: Equality implies equivalence of equalities. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
eqeq2  |-  ( A  =  B  ->  ( C  =  A  <->  C  =  B ) )

Proof of Theorem eqeq2
StepHypRef Expression
1 eqeq1 2062 . 2  |-  ( A  =  B  ->  ( A  =  C  <->  B  =  C ) )
2 eqcom 2058 . 2  |-  ( C  =  A  <->  A  =  C )
3 eqcom 2058 . 2  |-  ( C  =  B  <->  B  =  C )
41, 2, 33bitr4g 216 1  |-  ( A  =  B  ->  ( C  =  A  <->  C  =  B ) )
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  2693  ceqex  2694  pm13.183  2704  eqeu  2734  mo2icl  2743  mob2  2744  euind  2751  reu6i  2755  reuind  2767  sbc5  2810  csbiebg  2917  sneq  3414  preqr1g  3565  preqr1  3567  prel12  3570  preq12bg  3572  opth  4002  euotd  4019  ordtriexmid  4275  wetriext  4329  tfisi  4338  ideqg  4515  resieq  4650  cnveqb  4804  cnveq0  4805  iota5  4915  funopg  4962  fneq2  5016  foeq3  5132  tz6.12f  5230  funbrfv  5240  fnbrfvb  5242  fvelimab  5257  elrnrexdm  5334  eufnfv  5417  f1veqaeq  5436  mpt2eq123  5592  ovmpt4g  5651  ovi3  5665  ovg  5667  caovcang  5690  caovcan  5693  nntri3or  6103  nnaordex  6131  nnawordex  6132  ereq2  6145  eroveu  6228  2dom  6316  fundmen  6317  nneneq  6351  supsnti  6409  isotilem  6410  nqtri3or  6552  ltexnqq  6564  aptisr  6921  srpospr  6925  axpre-apti  7017  nntopi  7026  subval  7266  divvalap  7727  nn0ind-raph  8414  frecuzrdgfn  9362  sqrtrval  9827  divides  10110  dvdstr  10144  odd2np1lem  10183  ndvdssub  10242
  Copyright terms: Public domain W3C validator