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  6506  genpassu  6507  addcomprg  6553  mulcomprg  6555  distrlem1prl  6557  distrlem1pru  6558  distrlem5prl  6561  distrlem5pru  6562  1idprl  6565  1idpru  6566  recexprlem1ssl  6604  recexprlem1ssu  6605  addsrmo  6651  mulsrmo  6652  addsrpr  6653  mulsrpr  6654  elreal  6707  axcnre  6745  negeu  6979  subeq0  7013  apreap  7351  apreim  7367  divmulap3  7418  diveqap0  7423  diveqap1  7444  nn0ind-raph  8111  elq  8313  zq  8317  cnref1o  8337  iccf1o  8622  fzen  8657  fseq1m1p1  8707  fzm1  8712  nn0ennn  8870  bj-nn0suc0  9384  bj-inf2vnlem1  9400  bj-nn0sucALT  9408
  Copyright terms: Public domain W3C validator