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

Theorem eqeq2d 2033
Description: Deduction from equality to equivalence of equalities. (Contributed by NM, 27-Dec-1993.)
Hypothesis
Ref Expression
eqeq2d.1 (φA = B)
Assertion
Ref Expression
eqeq2d (φ → (𝐶 = A𝐶 = B))

Proof of Theorem eqeq2d
StepHypRef Expression
1 eqeq2d.1 . 2 (φA = B)
2 eqeq2 2031 . 2 (A = B → (𝐶 = A𝐶 = B))
31, 2syl 14 1 (φ → (𝐶 = A𝐶 = B))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 98   = wceq 1228
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1316  ax-gen 1318  ax-4 1381  ax-17 1400  ax-ext 2004
This theorem depends on definitions:  df-bi 110  df-cleq 2015
This theorem is referenced by:  eqtrd  2054  eq2tri  2081  sbceq1g  2847  euabsn  3414  absneu  3416  preq12bg  3518  cbvopab  3802  cbvopab1  3804  cbvopab2  3805  cbvopab1s  3806  cbvopab2v  3808  mpteq12f  3811  cbvmpt  3825  opth  3948  eqvinop  3954  moop2  3962  euotd  3965  eusvnf  4135  reusv3i  4141  nlimsucg  4226  nn0suc  4254  opelxp  4301  elvvv  4330  relop  4413  elrnmpt1s  4511  elrnmpt1  4512  elsnres  4574  elxp4  4735  elxp5  4736  relresfld  4774  iotajust  4793  iota1  4808  iota2df  4818  funopg  4860  funcnvuni  4894  fun11iun  5072  funcocnv2  5076  nfvres  5131  ssimaex  5159  fvmptg  5173  fvmptdf  5183  fvopab6  5189  foco2  5243  fmptco  5255  fsng  5261  elabrex  5322  abrexco  5323  f1veqaeq  5333  dff13f  5334  f1ocnvfv  5344  f1ocnvfvb  5345  fcofo  5349  fliftfun  5361  fliftval  5365  f1oiso2  5391  riota5f  5416  oprabid  5461  rspceov  5470  dfoprab2  5475  mpt2eq123dva  5489  mpt2eq3dva  5492  cbvoprab1  5499  cbvoprab2  5500  cbvoprab12  5501  cbvmpt2x  5505  mpt2mptx  5518  ovmpt2s  5547  ovmpt2df  5555  ovmpt2dv2  5557  ovi3  5560  ov6g  5561  fnrnov  5569  foov  5570  caovcang  5585  caovcan  5588  f1opw2  5629  opabex3d  5671  opabex3  5672  fo1st  5707  fo2nd  5708  elxp6  5719  op1steq  5728  dfoprab4f  5742  fmpt2x  5749  df1st2  5763  df2nd2  5764  xporderlem  5774  brtpos2  5788  dftpos4  5800  tposfn2  5803  recseq  5843  frecsuc  5907  nna0r  5972  eqerlem  6048  qseq2  6066  ecelqsg  6070  snec  6078  qsinxp  6093  ecoptocl  6104  eroveu  6108  th3qlem1  6119  th3qlem2  6120  th3q  6122  dfplpq2  6213  dfmpq2  6214  enqbreq2  6216  enq0sym  6287  enq0ref  6288  enq0tr  6289  addnq0mo  6302  mulnq0mo  6303  addnnnq0  6304  mulnnnq0  6305  nqnq0a  6309  nqnq0m  6310  nq0a0  6312  prarloclemcalc  6356  genipv  6363  genpassl  6379  genpassu  6380  addcomprg  6417  mulcomprg  6419  distrlem1prl  6421  distrlem1pru  6422  distrlem5prl  6425  distrlem5pru  6426  1idprl  6429  1idpru  6430  recexprlem1ssl  6467  recexprlem1ssu  6468  addsrmo  6490  mulsrmo  6491  addsrpr  6492  mulsrpr  6493  elreal  6541  axcnre  6575  negeu  6795  subeq0  6829  bj-nn0suc0  7319  bj-inf2vnlem1  7335  bj-nn0sucALT  7343
  Copyright terms: Public domain W3C validator