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

Theorem eqeq2d 2152
 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 2150 . 2 (𝐴 = 𝐵 → (𝐶 = 𝐴𝐶 = 𝐵))
31, 2syl 14 1 (𝜑 → (𝐶 = 𝐴𝐶 = 𝐵))
 Colors of variables: wff set class Syntax hints:   → wi 4   ↔ wb 104   = wceq 1332 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 1424  ax-gen 1426  ax-4 1488  ax-17 1507  ax-ext 2122 This theorem depends on definitions:  df-bi 116  df-cleq 2133 This theorem is referenced by:  eqtrd  2173  eq2tri  2200  rspcedeq2vd  2803  rspceeqv  2811  sbceq1g  3027  euabsn  3601  absneu  3603  preq12bg  3708  cbvopab  4007  cbvopab1  4009  cbvopab2  4010  cbvopab1s  4011  cbvopab2v  4013  mpteq12f  4016  cbvmptf  4030  cbvmpt  4031  exmidsssn  4133  exmidsssnc  4134  opth  4167  eqvinop  4173  moop2  4181  euotd  4184  eusvnf  4382  reusv3i  4388  nlimsucg  4489  nn0suc  4526  opelxp  4577  elvvv  4610  relop  4697  elrnmpt1s  4797  elrnmpt1  4798  elsnres  4864  elxp4  5034  elxp5  5035  relresfld  5076  iotajust  5095  iota1  5110  iota2df  5120  funopg  5165  funcnvuni  5200  fun11iun  5396  funcocnv2  5400  nfvres  5462  ssimaex  5490  fvmptg  5505  fvmptdf  5516  fvopab6  5525  fmptco  5594  fsng  5601  foco2  5663  elabrex  5667  abrexco  5668  f1veqaeq  5678  dff13f  5679  f1ocnvfv  5688  f1ocnvfvb  5689  fcofo  5693  fliftfun  5705  fliftval  5709  f1oiso2  5736  riota5f  5762  oprabid  5811  rspceov  5821  dfoprab2  5826  mpoeq123dva  5840  mpoeq3dva  5843  cbvoprab1  5851  cbvoprab2  5852  cbvoprab12  5853  cbvmpox  5857  mpomptx  5870  ovmpos  5902  ovmpodf  5910  ovmpodv2  5912  ovi3  5915  ov6g  5916  fnrnov  5924  foov  5925  caovcang  5940  caovcan  5943  f1opw2  5984  opabex3d  6027  opabex3  6028  fo1st  6063  fo2nd  6064  elxp6  6075  op1steq  6085  dfoprab4f  6099  fmpox  6106  fnmpoovd  6120  df1st2  6124  df2nd2  6125  xporderlem  6136  cnvoprab  6139  f1od2  6140  brtpos2  6156  dftpos4  6168  tposfn2  6171  recseq  6211  tfr1onlemaccex  6253  tfrcllemaccex  6266  frecabcl  6304  frecsuc  6312  nna0r  6382  eqerlem  6468  qseq2  6486  ecelqsg  6490  snec  6498  qsinxp  6513  ecoptocl  6524  eroveu  6528  th3qlem1  6539  th3qlem2  6540  th3q  6542  mapsncnv  6597  elixpsn  6637  ixpsnf1o  6638  en1  6701  mapsnen  6713  xpsnen  6723  xpassen  6732  xpf1o  6746  mapen  6748  mapxpen  6750  fidifsnen  6772  ac6sfi  6800  undifdc  6820  djuf1olem  6946  djur  6962  updjud  6975  omp1eomlem  6987  0ct  7000  enumctlemm  7007  fodjuomnilemdc  7024  fodjuomni  7029  fodjumkv  7042  exmidfodomrlemeldju  7073  exmidfodomrlemreseldju  7074  cc2lem  7099  dfplpq2  7187  dfmpq2  7188  enqbreq2  7190  enq0sym  7265  enq0ref  7266  enq0tr  7267  addnq0mo  7280  mulnq0mo  7281  addnnnq0  7282  mulnnnq0  7283  nqnq0a  7287  nqnq0m  7288  nq0a0  7290  prarloclemcalc  7335  genipv  7342  genpassl  7357  genpassu  7358  addcomprg  7411  mulcomprg  7413  distrlem1prl  7415  distrlem1pru  7416  distrlem5prl  7419  distrlem5pru  7420  1idprl  7423  1idpru  7424  recexprlem1ssl  7466  recexprlem1ssu  7467  addsrmo  7576  mulsrmo  7577  addsrpr  7578  mulsrpr  7579  elreal  7661  axcnre  7714  axcaucvglemval  7730  negeu  7978  subeq0  8013  apreap  8374  apreim  8390  divmulap3  8462  diveqap0  8467  diveqap1  8490  nn0ind-raph  9193  elq  9442  zq  9446  elpq  9468  cnref1o  9470  iccf1o  9818  fzen  9855  fseq1m1p1  9907  fzm1  9912  modqmuladd  10171  modqmuladdnn0  10173  modfzo0difsn  10200  nn0ennn  10238  seq3id2  10314  bcval5  10542  fihashen1  10578  shftlem  10621  shftfvalg  10623  shftfval  10626  negfi  11032  xrmaxiflemcom  11051  xrnegiso  11064  xrnegcon1d  11066  sumeq2  11161  summodc  11185  fsum3  11189  fsum2dlemstep  11236  isumsplit  11293  mertenslemub  11336  mertensabs  11339  prodeq2w  11358  prodeq2  11359  prodmodc  11380  fprodseq  11385  moddvds  11539  dvdsnegb  11547  dvdsabseq  11582  dvdsmod  11597  odd2np1lem  11606  odd2np1  11607  opeo  11631  omeo  11632  divalglemnn  11652  divalglemeunn  11655  divalglemex  11656  divalglemeuneg  11657  bezoutlemnewy  11721  bezoutlema  11724  bezoutlemb  11725  bezoutlemex  11726  bezoutlemaz  11728  bezoutlembz  11729  eucalglt  11775  qredeq  11814  qredeu  11815  divgcdcoprm0  11819  divgcdcoprmex  11820  cncongr1  11821  cncongr2  11822  qnumdenbi  11907  hashgcdlem  11940  evenennn  11943  ennnfonelemim  11974  istopon  12220  eltg3  12266  restsn  12389  txuni2  12465  txopn  12474  upxp  12481  uptx  12483  txrest  12485  hmeoimaf1o  12523  xmettxlem  12718  xmettx  12719  bj-nn0suc0  13320  bj-inf2vnlem1  13340  bj-nn0sucALT  13348  pwle2  13367  iooref1o  13437
 Copyright terms: Public domain W3C validator