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

Theorem eqeq12d 2051
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 (φA = B)
eqeq12d.2 (φ𝐶 = 𝐷)
Assertion
Ref Expression
eqeq12d (φ → (A = 𝐶B = 𝐷))

Proof of Theorem eqeq12d
StepHypRef Expression
1 eqeq12d.1 . 2 (φA = B)
2 eqeq12d.2 . 2 (φ𝐶 = 𝐷)
3 eqeq12 2049 . 2 ((A = B 𝐶 = 𝐷) → (A = 𝐶B = 𝐷))
41, 2, 3syl2anc 391 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:  cdeqeq  2753  sbceqg  2860  csbing  3138  uniprg  3586  unisng  3588  intprg  3639  iununir  3729  csbopabg  3826  limeq  4080  ordpwsucexmid  4246  csbima12g  4629  dmsnsnsng  4741  cnvsng  4749  csbiotag  4838  fvmptf  5206  eqfnfv2f  5212  fvreseq  5214  fmptco  5273  fnressn  5292  fvsng  5302  cocan1  5370  cocan2  5371  fliftfun  5379  csbriotag  5423  csbov123g  5485  eqfnov  5549  ovmpt2s  5566  ov2gf  5567  ovmpt2dxf  5568  caovcomg  5598  caovassg  5601  caovcang  5604  caovcanrd  5606  caovcan  5607  caovdig  5617  caovdirg  5620  caovimo  5636  grprinvlem  5637  grprinvd  5638  offveqb  5672  op1stg  5719  op2ndg  5720  f1o2ndf1  5791  tfrlem1  5864  tfrlem3ag  5865  tfrlem3a  5866  tfrlem5  5871  tfrlem9  5876  tfr0  5878  tfrlemiubacc  5885  tfrlemiex  5886  tfrlemi1  5887  tfri3  5894  rdg0g  5915  frecrdg  5931  nna0r  5996  nnacom  6002  nnaass  6003  nndi  6004  nnmass  6005  nnmsucr  6006  nnmcom  6007  ecopovtrn  6139  ecopovsymg  6141  ecopovtrng  6142  ecovcom  6149  ecovicom  6150  ecovass  6151  ecoviass  6152  ecovdi  6153  ecovidi  6154  dom2lem  6188  addcanpig  6318  mulcanpig  6319  mulcmpblnq  6352  mulpipqqs  6357  ordpipqqs  6358  mulidnq  6373  enq0sym  6414  nqnq0  6423  mulcmpblnq0  6426  distrnq0  6441  mulcomnq0  6442  addassnq0  6444  nq02m  6447  genipv  6491  cauappcvgprlemladd  6629  addcmpblnr  6647  0idsr  6675  1idsr  6676  axaddcom  6734  ax1rid  6741  ax0id  6742  mulid1  6802  readdcan  6930  cnegexlem1  6963  cnegexlem3  6965  addcan  6968  addcan2  6969  apti  7386  mulcanapd  7404  mulcanap2d  7405  div11ap  7439  divmuleqap  7455  conjmulap  7467  eqneg  7470  cnref1o  8337  fzsuc2  8691  fzprval  8694  fztpval  8695  frec2uzrdg  8856  iseqfveq2  8885  iseqfveq  8887  mulexp  8928  expadd  8931  expmul  8934  replim  9067  cjreb  9074  cjexp  9101
  Copyright terms: Public domain W3C validator