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

Theorem eqeq2d 2127
Description: Deduction from equality to equivalence of equalities. (Contributed by NM, 27-Dec-1993.)
Hypothesis
Ref Expression
eqeq2d.1  |-  ( ph  ->  A  =  B )
Assertion
Ref Expression
eqeq2d  |-  ( ph  ->  ( C  =  A  <-> 
C  =  B ) )

Proof of Theorem eqeq2d
StepHypRef Expression
1 eqeq2d.1 . 2  |-  ( ph  ->  A  =  B )
2 eqeq2 2125 . 2  |-  ( A  =  B  ->  ( C  =  A  <->  C  =  B ) )
31, 2syl 14 1  |-  ( ph  ->  ( C  =  A  <-> 
C  =  B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 104    = wceq 1314
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 1406  ax-gen 1408  ax-4 1470  ax-17 1489  ax-ext 2097
This theorem depends on definitions:  df-bi 116  df-cleq 2108
This theorem is referenced by:  eqtrd  2148  eq2tri  2175  rspcedeq2vd  2771  rspceeqv  2779  sbceq1g  2991  euabsn  3561  absneu  3563  preq12bg  3668  cbvopab  3967  cbvopab1  3969  cbvopab2  3970  cbvopab1s  3971  cbvopab2v  3973  mpteq12f  3976  cbvmptf  3990  cbvmpt  3991  exmidsssn  4093  exmidsssnc  4094  opth  4127  eqvinop  4133  moop2  4141  euotd  4144  eusvnf  4342  reusv3i  4348  nlimsucg  4449  nn0suc  4486  opelxp  4537  elvvv  4570  relop  4657  elrnmpt1s  4757  elrnmpt1  4758  elsnres  4824  elxp4  4994  elxp5  4995  relresfld  5036  iotajust  5055  iota1  5070  iota2df  5080  funopg  5125  funcnvuni  5160  fun11iun  5354  funcocnv2  5358  nfvres  5420  ssimaex  5448  fvmptg  5463  fvmptdf  5474  fvopab6  5483  fmptco  5552  fsng  5559  foco2  5621  elabrex  5625  abrexco  5626  f1veqaeq  5636  dff13f  5637  f1ocnvfv  5646  f1ocnvfvb  5647  fcofo  5651  fliftfun  5663  fliftval  5667  f1oiso2  5694  riota5f  5720  oprabid  5769  rspceov  5779  dfoprab2  5784  mpoeq123dva  5798  mpoeq3dva  5801  cbvoprab1  5809  cbvoprab2  5810  cbvoprab12  5811  cbvmpox  5815  mpomptx  5828  ovmpos  5860  ovmpodf  5868  ovmpodv2  5870  ovi3  5873  ov6g  5874  fnrnov  5882  foov  5883  caovcang  5898  caovcan  5901  f1opw2  5942  opabex3d  5985  opabex3  5986  fo1st  6021  fo2nd  6022  elxp6  6033  op1steq  6043  dfoprab4f  6057  fmpox  6064  fnmpoovd  6078  df1st2  6082  df2nd2  6083  xporderlem  6094  cnvoprab  6097  f1od2  6098  brtpos2  6114  dftpos4  6126  tposfn2  6129  recseq  6169  tfr1onlemaccex  6211  tfrcllemaccex  6224  frecabcl  6262  frecsuc  6270  nna0r  6340  eqerlem  6426  qseq2  6444  ecelqsg  6448  snec  6456  qsinxp  6471  ecoptocl  6482  eroveu  6486  th3qlem1  6497  th3qlem2  6498  th3q  6500  mapsncnv  6555  elixpsn  6595  ixpsnf1o  6596  en1  6659  mapsnen  6671  xpsnen  6681  xpassen  6690  xpf1o  6704  mapen  6706  mapxpen  6708  fidifsnen  6730  ac6sfi  6758  undifdc  6778  djuf1olem  6904  djur  6920  updjud  6933  omp1eomlem  6945  0ct  6958  enumctlemm  6965  fodjuomnilemdc  6982  fodjuomni  6987  fodjumkv  7000  exmidfodomrlemeldju  7019  exmidfodomrlemreseldju  7020  dfplpq2  7126  dfmpq2  7127  enqbreq2  7129  enq0sym  7204  enq0ref  7205  enq0tr  7206  addnq0mo  7219  mulnq0mo  7220  addnnnq0  7221  mulnnnq0  7222  nqnq0a  7226  nqnq0m  7227  nq0a0  7229  prarloclemcalc  7274  genipv  7281  genpassl  7296  genpassu  7297  addcomprg  7350  mulcomprg  7352  distrlem1prl  7354  distrlem1pru  7355  distrlem5prl  7358  distrlem5pru  7359  1idprl  7362  1idpru  7363  recexprlem1ssl  7405  recexprlem1ssu  7406  addsrmo  7515  mulsrmo  7516  addsrpr  7517  mulsrpr  7518  elreal  7600  axcnre  7653  axcaucvglemval  7669  negeu  7917  subeq0  7952  apreap  8312  apreim  8328  divmulap3  8397  diveqap0  8402  diveqap1  8425  nn0ind-raph  9119  elq  9363  zq  9367  cnref1o  9389  iccf1o  9727  fzen  9763  fseq1m1p1  9815  fzm1  9820  modqmuladd  10079  modqmuladdnn0  10081  modfzo0difsn  10108  nn0ennn  10146  seq3id2  10222  bcval5  10449  fihashen1  10485  shftlem  10528  shftfvalg  10530  shftfval  10533  negfi  10939  xrmaxiflemcom  10958  xrnegiso  10971  xrnegcon1d  10973  sumeq2  11068  summodc  11092  fsum3  11096  fsum2dlemstep  11143  isumsplit  11200  mertenslemub  11243  mertensabs  11246  moddvds  11398  dvdsnegb  11406  dvdsabseq  11441  dvdsmod  11456  odd2np1lem  11465  odd2np1  11466  opeo  11490  omeo  11491  divalglemnn  11511  divalglemeunn  11514  divalglemex  11515  divalglemeuneg  11516  bezoutlemnewy  11580  bezoutlema  11583  bezoutlemb  11584  bezoutlemex  11585  bezoutlemaz  11587  bezoutlembz  11588  eucalglt  11634  qredeq  11673  qredeu  11674  divgcdcoprm0  11678  divgcdcoprmex  11679  cncongr1  11680  cncongr2  11681  qnumdenbi  11765  hashgcdlem  11798  evenennn  11801  ennnfonelemim  11832  istopon  12075  eltg3  12121  restsn  12244  txuni2  12320  txopn  12329  upxp  12336  uptx  12338  txrest  12340  hmeoimaf1o  12378  xmettxlem  12573  xmettx  12574  bj-nn0suc0  12950  bj-inf2vnlem1  12970  bj-nn0sucALT  12978  pwle2  12995
  Copyright terms: Public domain W3C validator