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

Theorem eqeq12d 2155
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 (𝜑𝐶 = 𝐷)
Assertion
Ref Expression
eqeq12d (𝜑 → (𝐴 = 𝐶𝐵 = 𝐷))

Proof of Theorem eqeq12d
StepHypRef Expression
1 eqeq12d.1 . 2 (𝜑𝐴 = 𝐵)
2 eqeq12d.2 . 2 (𝜑𝐶 = 𝐷)
3 eqeq12 2153 . 2 ((𝐴 = 𝐵𝐶 = 𝐷) → (𝐴 = 𝐶𝐵 = 𝐷))
41, 2, 3syl2anc 409 1 (𝜑 → (𝐴 = 𝐶𝐵 = 𝐷))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 104   = wceq 1332
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1424  ax-gen 1426  ax-4 1488  ax-17 1507  ax-ext 2122
This theorem depends on definitions:  df-bi 116  df-cleq 2133
This theorem is referenced by:  cdeqeq  2907  sbceqg  3022  csbing  3287  uniprg  3758  unisng  3760  intprg  3811  iununir  3903  csbopabg  4013  undifexmid  4124  exmidundif  4136  exmidundifim  4137  limeq  4306  onsucuni2  4486  ordpwsucexmid  4492  csbima12g  4907  dmsnsnsng  5023  cnvsng  5031  csbiotag  5123  fvmptf  5520  eqfnfv2f  5529  fvreseq  5531  fmptco  5593  fnressn  5613  fvsng  5623  cocan1  5695  cocan2  5696  fliftfun  5704  csbriotag  5749  csbov123g  5816  eqfnov  5884  ovmpos  5901  ov2gf  5902  ovmpodxf  5903  caovcomg  5933  caovassg  5936  caovcang  5939  caovcanrd  5941  caovcan  5942  caovdig  5952  caovdirg  5955  caovimo  5971  grprinvlem  5972  grprinvd  5973  offveqb  6008  op1stg  6055  op2ndg  6056  f1o2ndf1  6132  tfrlem1  6212  tfrlem3ag  6213  tfrlem3a  6214  tfrlem5  6218  tfrlem9  6223  tfr0dm  6226  tfrlemiubacc  6234  tfrlemiex  6235  tfrlemi1  6236  tfr1onlem3ag  6241  tfr1onlemubacc  6250  tfr1onlemex  6251  tfr1onlemaccex  6252  tfrcllemsucaccv  6258  tfrcllembxssdm  6260  tfrcllemubacc  6263  tfrcllemex  6264  tfrcllemaccex  6265  tfrcllemres  6266  tfrcldm  6267  tfri3  6271  rdg0g  6292  frecrdg  6312  nna0r  6381  nnacom  6387  nnaass  6388  nndi  6389  nnmass  6390  nnmsucr  6391  nnmcom  6392  ecopovtrn  6533  ecopovsymg  6535  ecopovtrng  6536  ecovcom  6543  ecovicom  6544  ecovass  6545  ecoviass  6546  ecovdi  6547  ecovidi  6548  dom2lem  6673  ordiso2  6927  inl11  6957  updjud  6974  omp1eomlem  6986  difinfsnlem  6991  exmidfodomrlemrALT  7075  exmidaclem  7080  addcanpig  7165  mulcanpig  7166  mulcmpblnq  7199  mulpipqqs  7204  ordpipqqs  7205  mulidnq  7220  enq0sym  7263  nqnq0  7272  mulcmpblnq0  7275  distrnq0  7290  mulcomnq0  7291  addassnq0  7293  nq02m  7296  genipv  7340  cauappcvgprlemladd  7489  addcmpblnr  7570  0idsr  7598  1idsr  7599  axaddcom  7701  ax1rid  7708  ax0id  7709  rereceu  7720  axcaucvg  7731  mulid1  7786  readdcan  7925  cnegexlem1  7960  cnegexlem3  7962  addcan  7965  addcan2  7966  apti  8407  mulcanapd  8445  mulcanap2d  8446  div11ap  8483  divmuleqap  8500  conjmulap  8512  eqneg  8515  cnref1o  9468  fzsuc2  9889  fzprval  9892  fztpval  9893  qtri3or  10050  modqadd1  10164  modqmul1  10180  addmodlteq  10201  frec2uzrdg  10212  frecuzrdgg  10219  seq3val  10261  seqvalcd  10262  seq3fveq2  10272  seq3fveq  10274  seq3feq  10275  seq3shft2  10276  seq3split  10282  seq3caopr3  10284  seq3caopr2  10285  iseqf1olemkle  10287  iseqf1olemklt  10288  iseqf1olemqk  10297  seq3f1olemqsum  10303  seq3f1olemstep  10304  seq3f1olemp  10305  seq3f1oleml  10306  seq3id  10311  seq3id2  10312  seq3homo  10313  mulexp  10362  expadd  10365  expmul  10368  nn0opth2d  10500  bcpasc  10543  hashennn  10557  hashen  10561  omgadd  10579  hashfzo  10599  hashfzp1  10601  hashxp  10603  hashfacen  10610  seq3coll  10616  shftvalg  10639  shftval4g  10640  replim  10662  cjreb  10669  cjexp  10696  absexp  10882  recan  10912  minclpr  11039  sumeq2  11159  zsumdc  11184  fsum3  11187  fsumf1o  11190  fsum3cvg2  11194  fsumadd  11206  isummulc2  11226  fsum2d  11235  fsummulc2  11248  fsumconst  11254  modfsummod  11258  fsumparts  11270  fsumrelem  11271  fsumiun  11277  binom  11284  bcxmas  11289  isumshft  11290  isumnn0nn  11293  mertenslem2  11336  clim2prod  11339  prodfrecap  11346  prodeq2  11357  zproddc  11379  efne0  11419  efexp  11423  demoivreALT  11514  moddvds  11536  gcddiv  11741  alginv  11762  algfx  11767  lcmneg  11789  lcmid  11795  lcmgcdeq  11798  divgcdcoprm0  11816  cncongr1  11818  cncongr2  11819  nn0gcdsq  11912  crth  11934  txcnp  12477  cnmpt11  12489  cnmpt21  12497  cnmptcom  12504  isxms  12657  xmspropd  12683  bdmopn  12710  dvexp  12881  nninfalllemn  13375  nninffeq  13389
  Copyright terms: Public domain W3C validator