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

Theorem eqeq2 2094
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 2091 . 2  |-  ( A  =  B  ->  ( A  =  C  <->  B  =  C ) )
2 eqcom 2087 . 2  |-  ( C  =  A  <->  A  =  C )
3 eqcom 2087 . 2  |-  ( C  =  B  <->  B  =  C )
41, 2, 33bitr4g 221 1  |-  ( A  =  B  ->  ( C  =  A  <->  C  =  B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 103    = wceq 1287
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1379  ax-gen 1381  ax-4 1443  ax-17 1462  ax-ext 2067
This theorem depends on definitions:  df-bi 115  df-cleq 2078
This theorem is referenced by:  eqeq2i  2095  eqeq2d  2096  eqeq12  2097  eleq1  2147  neeq2  2265  alexeq  2734  ceqex  2735  pm13.183  2745  eqeu  2776  mo2icl  2785  mob2  2786  euind  2793  reu6i  2797  reuind  2809  sbc5  2852  csbiebg  2959  sneq  3442  preqr1g  3595  preqr1  3597  prel12  3600  preq12bg  3602  opth  4040  euotd  4057  ordtriexmid  4313  wetriext  4367  tfisi  4377  ideqg  4557  resieq  4693  cnveqb  4854  cnveq0  4855  iota5  4968  funopg  5015  fneq2  5070  foeq3  5196  tz6.12f  5298  funbrfv  5308  fnbrfvb  5310  fvelimab  5325  elrnrexdm  5403  eufnfv  5488  f1veqaeq  5511  mpt2eq123  5667  ovmpt4g  5726  ovi3  5740  ovg  5742  caovcang  5765  caovcan  5768  frecabcl  6120  nntri3or  6210  dcdifsnid  6219  nnaordex  6240  nnawordex  6241  ereq2  6254  eroveu  6337  2dom  6476  fundmen  6477  xpf1o  6514  nneneq  6527  tridc  6569  fisseneq  6595  supsnti  6647  isotilem  6648  updjud  6720  nqtri3or  6902  ltexnqq  6914  aptisr  7271  srpospr  7275  axpre-apti  7367  nntopi  7376  subval  7621  divvalap  8083  nn0ind-raph  8799  frecuzrdgtcl  9750  frecuzrdgfunlem  9757  sqrtrval  10332  isummolem2  10666  divides  10704  dvdstr  10739  odd2np1lem  10778  ndvdssub  10836  eucalglt  10945  hashgcdeq  11110
  Copyright terms: Public domain W3C validator