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

Theorem eqeq12d 2036
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 2034 . 2 ((A = B 𝐶 = 𝐷) → (A = 𝐶B = 𝐷))
41, 2, 3syl2anc 393 1 (φ → (A = 𝐶B = 𝐷))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 98   = wceq 1228
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 1316  ax-gen 1318  ax-4 1381  ax-17 1400  ax-ext 2004
This theorem depends on definitions:  df-bi 110  df-cleq 2015
This theorem is referenced by:  cdeqeq  2736  sbceqg  2843  csbing  3121  uniprg  3569  unisng  3571  intprg  3622  iununir  3712  csbopabg  3809  limeq  4063  ordpwsucexmid  4230  csbima12g  4613  dmsnsnsng  4725  cnvsng  4733  csbiotag  4822  fvmptf  5188  eqfnfv2f  5194  fvreseq  5196  fmptco  5255  fnressn  5274  fvsng  5284  cocan1  5352  cocan2  5353  fliftfun  5361  csbriotag  5404  csbov123g  5466  eqfnov  5530  ovmpt2s  5547  ov2gf  5548  ovmpt2dxf  5549  caovcomg  5579  caovassg  5582  caovcang  5585  caovcanrd  5587  caovcan  5588  caovdig  5598  caovdirg  5601  caovimo  5617  grprinvlem  5618  grprinvd  5619  offveqb  5653  op1stg  5700  op2ndg  5701  f1o2ndf1  5772  tfrlem1  5845  tfrlem3ag  5846  tfrlem3a  5847  tfrlem5  5852  tfrlem9  5857  tfrlemiubacc  5865  tfrlemiex  5866  tfrlemi1  5867  tfri3  5875  frecrdg  5908  nna0r  5972  nnacom  5978  nnaass  5979  nndi  5980  nnmass  5981  nnmsucr  5982  nnmcom  5983  ecopovtrn  6114  ecopovsymg  6116  ecopovtrng  6117  ecovcom  6124  ecovicom  6125  ecovass  6126  ecoviass  6127  ecovdi  6128  ecovidi  6129  addcanpig  6194  mulcanpig  6195  mulcmpblnq  6227  mulpipqqs  6232  ordpipqqs  6233  mulidnq  6248  enq0sym  6287  nqnq0  6296  mulcmpblnq0  6299  distrnq0  6314  mulcomnq0  6315  addassnq0  6317  nq02m  6319  genipv  6363  addcmpblnr  6486  0idsr  6514  1idsr  6515  axaddcom  6564  ax1rid  6571  ax0id  6572  mulid1  6626  readdcan  6740  cnegexlem1  6773  cnegexlem3  6775  addcan  6778  addcan2  6779
  Copyright terms: Public domain W3C validator