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

Theorem eqeq2d 2067
Description: Deduction from equality to equivalence of equalities. (Contributed by NM, 27-Dec-1993.)
Hypothesis
Ref Expression
eqeq2d.1  |-  ( ph  ->  A  =  B )
Assertion
Ref Expression
eqeq2d  |-  ( ph  ->  ( C  =  A  <-> 
C  =  B ) )

Proof of Theorem eqeq2d
StepHypRef Expression
1 eqeq2d.1 . 2  |-  ( ph  ->  A  =  B )
2 eqeq2 2065 . 2  |-  ( A  =  B  ->  ( C  =  A  <->  C  =  B ) )
31, 2syl 14 1  |-  ( ph  ->  ( C  =  A  <-> 
C  =  B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 102    = wceq 1259
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-5 1352  ax-gen 1354  ax-4 1416  ax-17 1435  ax-ext 2038
This theorem depends on definitions:  df-bi 114  df-cleq 2049
This theorem is referenced by:  eqtrd  2088  eq2tri  2115  rspcedeq2vd  2682  sbceq1g  2898  euabsn  3468  absneu  3470  preq12bg  3572  cbvopab  3856  cbvopab1  3858  cbvopab2  3859  cbvopab1s  3860  cbvopab2v  3862  mpteq12f  3865  cbvmpt  3879  opth  4002  eqvinop  4008  moop2  4016  euotd  4019  eusvnf  4213  reusv3i  4219  nlimsucg  4318  nn0suc  4355  opelxp  4402  elvvv  4431  relop  4514  elrnmpt1s  4612  elrnmpt1  4613  elsnres  4675  elxp4  4836  elxp5  4837  relresfld  4875  iotajust  4894  iota1  4909  iota2df  4919  funopg  4962  funcnvuni  4996  fun11iun  5175  funcocnv2  5179  nfvres  5234  ssimaex  5262  fvmptg  5276  fvmptdf  5286  fvopab6  5292  foco2  5346  fmptco  5358  fsng  5364  elabrex  5425  abrexco  5426  f1veqaeq  5436  dff13f  5437  f1ocnvfv  5447  f1ocnvfvb  5448  fcofo  5452  fliftfun  5464  fliftval  5468  f1oiso2  5494  riota5f  5520  oprabid  5565  rspceov  5575  dfoprab2  5580  mpt2eq123dva  5594  mpt2eq3dva  5597  cbvoprab1  5604  cbvoprab2  5605  cbvoprab12  5606  cbvmpt2x  5610  mpt2mptx  5623  ovmpt2s  5652  ovmpt2df  5660  ovmpt2dv2  5662  ovi3  5665  ov6g  5666  fnrnov  5674  foov  5675  caovcang  5690  caovcan  5693  f1opw2  5734  opabex3d  5776  opabex3  5777  fo1st  5812  fo2nd  5813  elxp6  5824  op1steq  5833  dfoprab4f  5847  fmpt2x  5854  df1st2  5868  df2nd2  5869  xporderlem  5880  cnvoprab  5883  f1od2  5884  brtpos2  5897  dftpos4  5909  tposfn2  5912  recseq  5952  frecsuc  6022  nna0r  6088  eqerlem  6168  qseq2  6186  ecelqsg  6190  snec  6198  qsinxp  6213  ecoptocl  6224  eroveu  6228  th3qlem1  6239  th3qlem2  6240  th3q  6242  en1  6310  xpsnen  6326  xpassen  6335  fidifsnen  6362  ac6sfi  6383  dfplpq2  6510  dfmpq2  6511  enqbreq2  6513  enq0sym  6588  enq0ref  6589  enq0tr  6590  addnq0mo  6603  mulnq0mo  6604  addnnnq0  6605  mulnnnq0  6606  nqnq0a  6610  nqnq0m  6611  nq0a0  6613  prarloclemcalc  6658  genipv  6665  genpassl  6680  genpassu  6681  addcomprg  6734  mulcomprg  6736  distrlem1prl  6738  distrlem1pru  6739  distrlem5prl  6742  distrlem5pru  6743  1idprl  6746  1idpru  6747  recexprlem1ssl  6789  recexprlem1ssu  6790  addsrmo  6886  mulsrmo  6887  addsrpr  6888  mulsrpr  6889  elreal  6963  axcnre  7013  axcaucvglemval  7029  negeu  7265  subeq0  7300  apreap  7652  apreim  7668  divmulap3  7730  diveqap0  7735  diveqap1  7756  nn0ind-raph  8414  elq  8654  zq  8658  cnref1o  8680  iccf1o  8973  fzen  9009  fseq1m1p1  9059  fzm1  9064  modqmuladd  9316  modqmuladdnn0  9318  modfzo0difsn  9345  nn0ennn  9373  ibcval5  9631  shftlem  9645  shftfvalg  9647  shftfval  9650  moddvds  10117  dvdsnegb  10125  dvdsabseq  10159  dvdsmod  10174  odd2np1lem  10183  odd2np1  10184  opeo  10209  omeo  10210  divalglemnn  10230  divalglemeunn  10233  divalglemex  10234  divalglemeuneg  10235  bj-nn0suc0  10462  bj-inf2vnlem1  10482  bj-nn0sucALT  10490
  Copyright terms: Public domain W3C validator