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

Theorem eqeq12d 2032
Description: A useful inference for substituting definitions into an equality. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.)
Hypotheses
Ref Expression
eqeq12d.1
eqeq12d.2  C  D
Assertion
Ref Expression
eqeq12d  C  D

Proof of Theorem eqeq12d
StepHypRef Expression
1 eqeq12d.1 . 2
2 eqeq12d.2 . 2  C  D
3 eqeq12 2030 . 2  C  D  C  D
41, 2, 3syl2anc 393 1  C  D
Colors of variables: wff set class
Syntax hints:   wi 4   wb 98   wceq 1226
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 1312  ax-gen 1314  ax-4 1377  ax-17 1396  ax-ext 2000
This theorem depends on definitions:  df-bi 110  df-cleq 2011
This theorem is referenced by:  cdeqeq  2732  sbceqg  2839  csbing  3117  uniprg  3565  unisng  3567  intprg  3618  iununir  3708  csbopabg  3805  limeq  4059  ordpwsucexmid  4226  csbima12g  4609  dmsnsnsng  4721  cnvsng  4729  csbiotag  4818  fvmptf  5184  eqfnfv2f  5190  fvreseq  5192  fmptco  5251  fnressn  5270  fvsng  5280  cocan1  5348  cocan2  5349  fliftfun  5357  csbriotag  5400  csbov123g  5462  eqfnov  5526  ovmpt2s  5543  ov2gf  5544  ovmpt2dxf  5545  caovcomg  5575  caovassg  5578  caovcang  5581  caovcanrd  5583  caovcan  5584  caovdig  5594  caovdirg  5597  caovimo  5613  grprinvlem  5614  grprinvd  5615  offveqb  5649  op1stg  5696  op2ndg  5697  f1o2ndf1  5768  tfrlem1  5841  tfrlem3ag  5842  tfrlem3a  5843  tfrlem5  5848  tfrlem9  5853  tfrlemiubacc  5861  tfrlemiex  5862  tfrlemi1  5863  tfri3  5871  frecrdg  5904  nna0r  5968  nnacom  5974  nnaass  5975  nndi  5976  nnmass  5977  nnmsucr  5978  nnmcom  5979  ecopovtrn  6110  ecopovsymg  6112  ecopovtrng  6113  ecovcom  6120  ecovicom  6121  ecovass  6122  ecoviass  6123  ecovdi  6124  ecovidi  6125  addcanpig  6188  mulcanpig  6189  mulcmpblnq  6221  mulpipqqs  6226  ordpipqqs  6227  mulidnq  6242  enq0sym  6281  nqnq0  6290  mulcmpblnq0  6293  distrnq0  6308  mulcomnq0  6309  addassnq0  6311  nq02m  6313  genipv  6357  addcmpblnr  6483  0idsr  6511  1idsr  6512  axaddcom  6563  ax1rid  6570  ax0id  6571  mulid1  6627  readdcan  6755  cnegexlem1  6788  cnegexlem3  6790  addcan  6793  addcan2  6794
  Copyright terms: Public domain W3C validator