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

Theorem eqeq2 2127
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 2124 . 2  |-  ( A  =  B  ->  ( A  =  C  <->  B  =  C ) )
2 eqcom 2119 . 2  |-  ( C  =  A  <->  A  =  C )
3 eqcom 2119 . 2  |-  ( C  =  B  <->  B  =  C )
41, 2, 33bitr4g 222 1  |-  ( A  =  B  ->  ( C  =  A  <->  C  =  B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 104    = wceq 1316
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 1408  ax-gen 1410  ax-4 1472  ax-17 1491  ax-ext 2099
This theorem depends on definitions:  df-bi 116  df-cleq 2110
This theorem is referenced by:  eqeq2i  2128  eqeq2d  2129  eqeq12  2130  eleq1  2180  neeq2  2299  alexeq  2785  ceqex  2786  pm13.183  2796  eqeu  2827  mo2icl  2836  mob2  2837  euind  2844  reu6i  2848  reuind  2862  sbc5  2905  csbiebg  3012  sneq  3508  preqr1g  3663  preqr1  3665  prel12  3668  preq12bg  3670  opth  4129  euotd  4146  ordtriexmid  4407  wetriext  4461  tfisi  4471  ideqg  4660  resieq  4799  cnveqb  4964  cnveq0  4965  iota5  5078  funopg  5127  fneq2  5182  foeq3  5313  tz6.12f  5418  funbrfv  5428  fnbrfvb  5430  fvelimab  5445  elrnrexdm  5527  eufnfv  5616  f1veqaeq  5638  mpoeq123  5798  ovmpt4g  5861  ovi3  5875  ovg  5877  caovcang  5900  caovcan  5903  frecabcl  6264  nntri3or  6357  dcdifsnid  6368  nnaordex  6391  nnawordex  6392  ereq2  6405  eroveu  6488  2dom  6667  fundmen  6668  xpf1o  6706  nneneq  6719  tridc  6761  fisseneq  6788  fidcenumlemrks  6809  supsnti  6860  isotilem  6861  updjud  6935  nqtri3or  7172  ltexnqq  7184  aptisr  7555  srpospr  7559  map2psrprg  7581  axpre-apti  7661  nntopi  7670  subval  7922  eqord1  8213  divvalap  8402  nn0ind-raph  9136  frecuzrdgtcl  10153  frecuzrdgfunlem  10160  sqrtrval  10740  summodclem2  11119  divides  11422  dvdstr  11457  odd2np1lem  11496  ndvdssub  11554  eucalglt  11665  hashgcdeq  11831  ennnfonelemim  11864  xmeteq0  12455  trilpo  13163
  Copyright terms: Public domain W3C validator