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  addcmpblnr  6627  0idsr  6655  1idsr  6656  axaddcom  6714  ax1rid  6721  ax0id  6722  mulid1  6782  readdcan  6910  cnegexlem1  6943  cnegexlem3  6945  addcan  6948  addcan2  6949  apti  7366  mulcanapd  7384  mulcanap2d  7385  div11ap  7419  divmuleqap  7435  conjmulap  7447  eqneg  7450  cnref1o  8317  fzsuc2  8671  fzprval  8674  fztpval  8675  frec2uzrdg  8836  iseqfveq2  8865  iseqfveq  8867  mulexp  8908  expadd  8911  expmul  8914  replim  9047  cjreb  9054  cjexp  9081
  Copyright terms: Public domain W3C validator