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

Theorem eqeq2d 2048
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 2046 . 2 (A = B → (𝐶 = A𝐶 = B))
31, 2syl 14 1 (φ → (𝐶 = A𝐶 = B))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 98   = wceq 1242
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 1333  ax-gen 1335  ax-4 1397  ax-17 1416  ax-ext 2019
This theorem depends on definitions:  df-bi 110  df-cleq 2030
This theorem is referenced by:  eqtrd  2069  eq2tri  2096  sbceq1g  2864  euabsn  3431  absneu  3433  preq12bg  3535  cbvopab  3819  cbvopab1  3821  cbvopab2  3822  cbvopab1s  3823  cbvopab2v  3825  mpteq12f  3828  cbvmpt  3842  opth  3965  eqvinop  3971  moop2  3979  euotd  3982  eusvnf  4151  reusv3i  4157  nlimsucg  4242  nn0suc  4270  opelxp  4317  elvvv  4346  relop  4429  elrnmpt1s  4527  elrnmpt1  4528  elsnres  4590  elxp4  4751  elxp5  4752  relresfld  4790  iotajust  4809  iota1  4824  iota2df  4834  funopg  4877  funcnvuni  4911  fun11iun  5090  funcocnv2  5094  nfvres  5149  ssimaex  5177  fvmptg  5191  fvmptdf  5201  fvopab6  5207  foco2  5261  fmptco  5273  fsng  5279  elabrex  5340  abrexco  5341  f1veqaeq  5351  dff13f  5352  f1ocnvfv  5362  f1ocnvfvb  5363  fcofo  5367  fliftfun  5379  fliftval  5383  f1oiso2  5409  riota5f  5435  oprabid  5480  rspceov  5489  dfoprab2  5494  mpt2eq123dva  5508  mpt2eq3dva  5511  cbvoprab1  5518  cbvoprab2  5519  cbvoprab12  5520  cbvmpt2x  5524  mpt2mptx  5537  ovmpt2s  5566  ovmpt2df  5574  ovmpt2dv2  5576  ovi3  5579  ov6g  5580  fnrnov  5588  foov  5589  caovcang  5604  caovcan  5607  f1opw2  5648  opabex3d  5690  opabex3  5691  fo1st  5726  fo2nd  5727  elxp6  5738  op1steq  5747  dfoprab4f  5761  fmpt2x  5768  df1st2  5782  df2nd2  5783  xporderlem  5793  brtpos2  5807  dftpos4  5819  tposfn2  5822  recseq  5862  frecsuc  5930  nna0r  5996  eqerlem  6073  qseq2  6091  ecelqsg  6095  snec  6103  qsinxp  6118  ecoptocl  6129  eroveu  6133  th3qlem1  6144  th3qlem2  6145  th3q  6147  en1  6215  xpsnen  6231  xpassen  6240  dfplpq2  6338  dfmpq2  6339  enqbreq2  6341  enq0sym  6414  enq0ref  6415  enq0tr  6416  addnq0mo  6429  mulnq0mo  6430  addnnnq0  6431  mulnnnq0  6432  nqnq0a  6436  nqnq0m  6437  nq0a0  6439  prarloclemcalc  6484  genipv  6491  genpassl  6507  genpassu  6508  addcomprg  6552  mulcomprg  6554  distrlem1prl  6556  distrlem1pru  6557  distrlem5prl  6560  distrlem5pru  6561  1idprl  6564  1idpru  6565  recexprlem1ssl  6603  recexprlem1ssu  6604  addsrmo  6631  mulsrmo  6632  addsrpr  6633  mulsrpr  6634  elreal  6687  axcnre  6725  negeu  6959  subeq0  6993  apreap  7331  apreim  7347  divmulap3  7398  diveqap0  7403  diveqap1  7424  nn0ind-raph  8091  elq  8293  zq  8297  cnref1o  8317  iccf1o  8602  fzen  8637  fseq1m1p1  8687  fzm1  8692  nn0ennn  8850  bj-nn0suc0  9338  bj-inf2vnlem1  9354  bj-nn0sucALT  9362
  Copyright terms: Public domain W3C validator