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

Theorem eqeq2d 2129
Description: Deduction from equality to equivalence of equalities. (Contributed by NM, 27-Dec-1993.)
Hypothesis
Ref Expression
eqeq2d.1 (𝜑𝐴 = 𝐵)
Assertion
Ref Expression
eqeq2d (𝜑 → (𝐶 = 𝐴𝐶 = 𝐵))

Proof of Theorem eqeq2d
StepHypRef Expression
1 eqeq2d.1 . 2 (𝜑𝐴 = 𝐵)
2 eqeq2 2127 . 2 (𝐴 = 𝐵 → (𝐶 = 𝐴𝐶 = 𝐵))
31, 2syl 14 1 (𝜑 → (𝐶 = 𝐴𝐶 = 𝐵))
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:  eqtrd  2150  eq2tri  2177  rspcedeq2vd  2773  rspceeqv  2781  sbceq1g  2993  euabsn  3563  absneu  3565  preq12bg  3670  cbvopab  3969  cbvopab1  3971  cbvopab2  3972  cbvopab1s  3973  cbvopab2v  3975  mpteq12f  3978  cbvmptf  3992  cbvmpt  3993  exmidsssn  4095  exmidsssnc  4096  opth  4129  eqvinop  4135  moop2  4143  euotd  4146  eusvnf  4344  reusv3i  4350  nlimsucg  4451  nn0suc  4488  opelxp  4539  elvvv  4572  relop  4659  elrnmpt1s  4759  elrnmpt1  4760  elsnres  4826  elxp4  4996  elxp5  4997  relresfld  5038  iotajust  5057  iota1  5072  iota2df  5082  funopg  5127  funcnvuni  5162  fun11iun  5356  funcocnv2  5360  nfvres  5422  ssimaex  5450  fvmptg  5465  fvmptdf  5476  fvopab6  5485  fmptco  5554  fsng  5561  foco2  5623  elabrex  5627  abrexco  5628  f1veqaeq  5638  dff13f  5639  f1ocnvfv  5648  f1ocnvfvb  5649  fcofo  5653  fliftfun  5665  fliftval  5669  f1oiso2  5696  riota5f  5722  oprabid  5771  rspceov  5781  dfoprab2  5786  mpoeq123dva  5800  mpoeq3dva  5803  cbvoprab1  5811  cbvoprab2  5812  cbvoprab12  5813  cbvmpox  5817  mpomptx  5830  ovmpos  5862  ovmpodf  5870  ovmpodv2  5872  ovi3  5875  ov6g  5876  fnrnov  5884  foov  5885  caovcang  5900  caovcan  5903  f1opw2  5944  opabex3d  5987  opabex3  5988  fo1st  6023  fo2nd  6024  elxp6  6035  op1steq  6045  dfoprab4f  6059  fmpox  6066  fnmpoovd  6080  df1st2  6084  df2nd2  6085  xporderlem  6096  cnvoprab  6099  f1od2  6100  brtpos2  6116  dftpos4  6128  tposfn2  6131  recseq  6171  tfr1onlemaccex  6213  tfrcllemaccex  6226  frecabcl  6264  frecsuc  6272  nna0r  6342  eqerlem  6428  qseq2  6446  ecelqsg  6450  snec  6458  qsinxp  6473  ecoptocl  6484  eroveu  6488  th3qlem1  6499  th3qlem2  6500  th3q  6502  mapsncnv  6557  elixpsn  6597  ixpsnf1o  6598  en1  6661  mapsnen  6673  xpsnen  6683  xpassen  6692  xpf1o  6706  mapen  6708  mapxpen  6710  fidifsnen  6732  ac6sfi  6760  undifdc  6780  djuf1olem  6906  djur  6922  updjud  6935  omp1eomlem  6947  0ct  6960  enumctlemm  6967  fodjuomnilemdc  6984  fodjuomni  6989  fodjumkv  7002  exmidfodomrlemeldju  7023  exmidfodomrlemreseldju  7024  dfplpq2  7130  dfmpq2  7131  enqbreq2  7133  enq0sym  7208  enq0ref  7209  enq0tr  7210  addnq0mo  7223  mulnq0mo  7224  addnnnq0  7225  mulnnnq0  7226  nqnq0a  7230  nqnq0m  7231  nq0a0  7233  prarloclemcalc  7278  genipv  7285  genpassl  7300  genpassu  7301  addcomprg  7354  mulcomprg  7356  distrlem1prl  7358  distrlem1pru  7359  distrlem5prl  7362  distrlem5pru  7363  1idprl  7366  1idpru  7367  recexprlem1ssl  7409  recexprlem1ssu  7410  addsrmo  7519  mulsrmo  7520  addsrpr  7521  mulsrpr  7522  elreal  7604  axcnre  7657  axcaucvglemval  7673  negeu  7921  subeq0  7956  apreap  8316  apreim  8332  divmulap3  8404  diveqap0  8409  diveqap1  8432  nn0ind-raph  9126  elq  9370  zq  9374  cnref1o  9396  iccf1o  9742  fzen  9778  fseq1m1p1  9830  fzm1  9835  modqmuladd  10094  modqmuladdnn0  10096  modfzo0difsn  10123  nn0ennn  10161  seq3id2  10237  bcval5  10464  fihashen1  10500  shftlem  10543  shftfvalg  10545  shftfval  10548  negfi  10954  xrmaxiflemcom  10973  xrnegiso  10986  xrnegcon1d  10988  sumeq2  11083  summodc  11107  fsum3  11111  fsum2dlemstep  11158  isumsplit  11215  mertenslemub  11258  mertensabs  11261  moddvds  11414  dvdsnegb  11422  dvdsabseq  11457  dvdsmod  11472  odd2np1lem  11481  odd2np1  11482  opeo  11506  omeo  11507  divalglemnn  11527  divalglemeunn  11530  divalglemex  11531  divalglemeuneg  11532  bezoutlemnewy  11596  bezoutlema  11599  bezoutlemb  11600  bezoutlemex  11601  bezoutlemaz  11603  bezoutlembz  11604  eucalglt  11650  qredeq  11689  qredeu  11690  divgcdcoprm0  11694  divgcdcoprmex  11695  cncongr1  11696  cncongr2  11697  qnumdenbi  11781  hashgcdlem  11814  evenennn  11817  ennnfonelemim  11848  istopon  12091  eltg3  12137  restsn  12260  txuni2  12336  txopn  12345  upxp  12352  uptx  12354  txrest  12356  hmeoimaf1o  12394  xmettxlem  12589  xmettx  12590  bj-nn0suc0  13044  bj-inf2vnlem1  13064  bj-nn0sucALT  13072  pwle2  13089
  Copyright terms: Public domain W3C validator