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

Theorem eqeq2d 2051
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 2049 . 2 (𝐴 = 𝐵 → (𝐶 = 𝐴𝐶 = 𝐵))
31, 2syl 14 1 (𝜑 → (𝐶 = 𝐴𝐶 = 𝐵))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 98   = wceq 1243
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 1336  ax-gen 1338  ax-4 1400  ax-17 1419  ax-ext 2022
This theorem depends on definitions:  df-bi 110  df-cleq 2033
This theorem is referenced by:  eqtrd  2072  eq2tri  2099  sbceq1g  2870  euabsn  3440  absneu  3442  preq12bg  3544  cbvopab  3828  cbvopab1  3830  cbvopab2  3831  cbvopab1s  3832  cbvopab2v  3834  mpteq12f  3837  cbvmpt  3851  opth  3974  eqvinop  3980  moop2  3988  euotd  3991  eusvnf  4185  reusv3i  4191  nlimsucg  4290  nn0suc  4327  opelxp  4374  elvvv  4403  relop  4486  elrnmpt1s  4584  elrnmpt1  4585  elsnres  4647  elxp4  4808  elxp5  4809  relresfld  4847  iotajust  4866  iota1  4881  iota2df  4891  funopg  4934  funcnvuni  4968  fun11iun  5147  funcocnv2  5151  nfvres  5206  ssimaex  5234  fvmptg  5248  fvmptdf  5258  fvopab6  5264  foco2  5318  fmptco  5330  fsng  5336  elabrex  5397  abrexco  5398  f1veqaeq  5408  dff13f  5409  f1ocnvfv  5419  f1ocnvfvb  5420  fcofo  5424  fliftfun  5436  fliftval  5440  f1oiso2  5466  riota5f  5492  oprabid  5537  rspceov  5547  dfoprab2  5552  mpt2eq123dva  5566  mpt2eq3dva  5569  cbvoprab1  5576  cbvoprab2  5577  cbvoprab12  5578  cbvmpt2x  5582  mpt2mptx  5595  ovmpt2s  5624  ovmpt2df  5632  ovmpt2dv2  5634  ovi3  5637  ov6g  5638  fnrnov  5646  foov  5647  caovcang  5662  caovcan  5665  f1opw2  5706  opabex3d  5748  opabex3  5749  fo1st  5784  fo2nd  5785  elxp6  5796  op1steq  5805  dfoprab4f  5819  fmpt2x  5826  df1st2  5840  df2nd2  5841  xporderlem  5852  brtpos2  5866  dftpos4  5878  tposfn2  5881  recseq  5921  frecsuc  5991  nna0r  6057  eqerlem  6137  qseq2  6155  ecelqsg  6159  snec  6167  qsinxp  6182  ecoptocl  6193  eroveu  6197  th3qlem1  6208  th3qlem2  6209  th3q  6211  en1  6279  xpsnen  6295  xpassen  6304  fidifsnen  6331  ac6sfi  6352  dfplpq2  6450  dfmpq2  6451  enqbreq2  6453  enq0sym  6528  enq0ref  6529  enq0tr  6530  addnq0mo  6543  mulnq0mo  6544  addnnnq0  6545  mulnnnq0  6546  nqnq0a  6550  nqnq0m  6551  nq0a0  6553  prarloclemcalc  6598  genipv  6605  genpassl  6620  genpassu  6621  addcomprg  6674  mulcomprg  6676  distrlem1prl  6678  distrlem1pru  6679  distrlem5prl  6682  distrlem5pru  6683  1idprl  6686  1idpru  6687  recexprlem1ssl  6729  recexprlem1ssu  6730  addsrmo  6826  mulsrmo  6827  addsrpr  6828  mulsrpr  6829  elreal  6903  axcnre  6953  axcaucvglemval  6969  negeu  7200  subeq0  7235  apreap  7576  apreim  7592  divmulap3  7654  diveqap0  7659  diveqap1  7680  nn0ind-raph  8353  elq  8555  zq  8559  cnref1o  8580  iccf1o  8870  fzen  8905  fseq1m1p1  8955  fzm1  8960  nn0ennn  9207  shftlem  9415  shftfvalg  9417  shftfval  9420  bj-nn0suc0  10073  bj-inf2vnlem1  10093  bj-nn0sucALT  10101
  Copyright terms: Public domain W3C validator