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  8317  apreim  8333  divmulap3  8405  diveqap0  8410  diveqap1  8433  nn0ind-raph  9136  elq  9382  zq  9386  cnref1o  9408  iccf1o  9755  fzen  9791  fseq1m1p1  9843  fzm1  9848  modqmuladd  10107  modqmuladdnn0  10109  modfzo0difsn  10136  nn0ennn  10174  seq3id2  10250  bcval5  10477  fihashen1  10513  shftlem  10556  shftfvalg  10558  shftfval  10561  negfi  10967  xrmaxiflemcom  10986  xrnegiso  10999  xrnegcon1d  11001  sumeq2  11096  summodc  11120  fsum3  11124  fsum2dlemstep  11171  isumsplit  11228  mertenslemub  11271  mertensabs  11274  moddvds  11429  dvdsnegb  11437  dvdsabseq  11472  dvdsmod  11487  odd2np1lem  11496  odd2np1  11497  opeo  11521  omeo  11522  divalglemnn  11542  divalglemeunn  11545  divalglemex  11546  divalglemeuneg  11547  bezoutlemnewy  11611  bezoutlema  11614  bezoutlemb  11615  bezoutlemex  11616  bezoutlemaz  11618  bezoutlembz  11619  eucalglt  11665  qredeq  11704  qredeu  11705  divgcdcoprm0  11709  divgcdcoprmex  11710  cncongr1  11711  cncongr2  11712  qnumdenbi  11797  hashgcdlem  11830  evenennn  11833  ennnfonelemim  11864  istopon  12107  eltg3  12153  restsn  12276  txuni2  12352  txopn  12361  upxp  12368  uptx  12370  txrest  12372  hmeoimaf1o  12410  xmettxlem  12605  xmettx  12606  bj-nn0suc0  13075  bj-inf2vnlem1  13095  bj-nn0sucALT  13103  pwle2  13120
  Copyright terms: Public domain W3C validator