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  3585  unisng  3587  intprg  3638  iununir  3728  csbopabg  3825  limeq  4079  ordpwsucexmid  4245  csbima12g  4628  dmsnsnsng  4740  cnvsng  4748  csbiotag  4837  fvmptf  5204  eqfnfv2f  5210  fvreseq  5212  fmptco  5271  fnressn  5290  fvsng  5300  cocan1  5368  cocan2  5369  fliftfun  5377  csbriotag  5420  csbov123g  5482  eqfnov  5546  ovmpt2s  5563  ov2gf  5564  ovmpt2dxf  5565  caovcomg  5595  caovassg  5598  caovcang  5601  caovcanrd  5603  caovcan  5604  caovdig  5614  caovdirg  5617  caovimo  5633  grprinvlem  5634  grprinvd  5635  offveqb  5669  op1stg  5716  op2ndg  5717  f1o2ndf1  5788  tfrlem1  5861  tfrlem3ag  5862  tfrlem3a  5863  tfrlem5  5868  tfrlem9  5873  tfr0  5875  tfrlemiubacc  5882  tfrlemiex  5883  tfrlemi1  5884  tfri3  5891  rdg0g  5912  frecrdg  5925  nna0r  5989  nnacom  5995  nnaass  5996  nndi  5997  nnmass  5998  nnmsucr  5999  nnmcom  6000  ecopovtrn  6132  ecopovsymg  6134  ecopovtrng  6135  ecovcom  6142  ecovicom  6143  ecovass  6144  ecoviass  6145  ecovdi  6146  ecovidi  6147  dom2lem  6181  addcanpig  6311  mulcanpig  6312  mulcmpblnq  6345  mulpipqqs  6350  ordpipqqs  6351  mulidnq  6366  enq0sym  6407  nqnq0  6416  mulcmpblnq0  6419  distrnq0  6434  mulcomnq0  6435  addassnq0  6437  nq02m  6440  genipv  6484  addcmpblnr  6619  0idsr  6647  1idsr  6648  axaddcom  6706  ax1rid  6713  ax0id  6714  mulid1  6774  readdcan  6902  cnegexlem1  6935  cnegexlem3  6937  addcan  6940  addcan2  6941  apti  7358  mulcanapd  7376  mulcanap2d  7377  div11ap  7411  divmuleqap  7427  conjmulap  7439  eqneg  7442  fzsuc2  8657  fzprval  8660  fztpval  8661
  Copyright terms: Public domain W3C validator