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

Theorem eqeq12d 2099
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 2097 . 2 ((𝐴 = 𝐵𝐶 = 𝐷) → (𝐴 = 𝐶𝐵 = 𝐷))
41, 2, 3syl2anc 403 1 (𝜑 → (𝐴 = 𝐶𝐵 = 𝐷))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 103   = wceq 1287
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1379  ax-gen 1381  ax-4 1443  ax-17 1462  ax-ext 2067
This theorem depends on definitions:  df-bi 115  df-cleq 2078
This theorem is referenced by:  cdeqeq  2824  sbceqg  2936  csbing  3196  uniprg  3651  unisng  3653  intprg  3704  iununir  3794  csbopabg  3891  undifexmid  4002  exmidundif  4009  limeq  4178  onsucuni2  4353  ordpwsucexmid  4359  csbima12g  4760  dmsnsnsng  4874  cnvsng  4882  csbiotag  4974  fvmptf  5358  eqfnfv2f  5364  fvreseq  5366  fmptco  5427  fnressn  5446  fvsng  5456  cocan1  5527  cocan2  5528  fliftfun  5536  csbriotag  5581  csbov123g  5644  eqfnov  5708  ovmpt2s  5725  ov2gf  5726  ovmpt2dxf  5727  caovcomg  5757  caovassg  5760  caovcang  5763  caovcanrd  5765  caovcan  5766  caovdig  5776  caovdirg  5779  caovimo  5795  grprinvlem  5796  grprinvd  5797  offveqb  5831  op1stg  5878  op2ndg  5879  f1o2ndf1  5950  tfrlem1  6027  tfrlem3ag  6028  tfrlem3a  6029  tfrlem5  6033  tfrlem9  6038  tfr0dm  6041  tfrlemiubacc  6049  tfrlemiex  6050  tfrlemi1  6051  tfr1onlem3ag  6056  tfr1onlemubacc  6065  tfr1onlemex  6066  tfr1onlemaccex  6067  tfrcllemsucaccv  6073  tfrcllembxssdm  6075  tfrcllemubacc  6078  tfrcllemex  6079  tfrcllemaccex  6080  tfrcllemres  6081  tfrcldm  6082  tfri3  6086  rdg0g  6107  frecrdg  6127  nna0r  6193  nnacom  6199  nnaass  6200  nndi  6201  nnmass  6202  nnmsucr  6203  nnmcom  6204  ecopovtrn  6341  ecopovsymg  6343  ecopovtrng  6344  ecovcom  6351  ecovicom  6352  ecovass  6353  ecoviass  6354  ecovdi  6355  ecovidi  6356  dom2lem  6441  ordiso2  6672  updjud  6717  exmidfodomrlemrALT  6773  addcanpig  6837  mulcanpig  6838  mulcmpblnq  6871  mulpipqqs  6876  ordpipqqs  6877  mulidnq  6892  enq0sym  6935  nqnq0  6944  mulcmpblnq0  6947  distrnq0  6962  mulcomnq0  6963  addassnq0  6965  nq02m  6968  genipv  7012  cauappcvgprlemladd  7161  addcmpblnr  7229  0idsr  7257  1idsr  7258  axaddcom  7349  ax1rid  7356  ax0id  7357  rereceu  7368  axcaucvg  7379  mulid1  7429  readdcan  7566  cnegexlem1  7601  cnegexlem3  7603  addcan  7606  addcan2  7607  apti  8040  mulcanapd  8069  mulcanap2d  8070  div11ap  8106  divmuleqap  8123  conjmulap  8135  eqneg  8138  cnref1o  9065  fzsuc2  9423  fzprval  9426  fztpval  9427  qtri3or  9582  modqadd1  9696  modqmul1  9712  addmodlteq  9733  frec2uzrdg  9744  frecuzrdgg  9751  iseqvalt  9790  iseqoveq  9798  iseqss  9799  iseqsst  9800  iseqfveq2  9802  iseqfveq  9804  iseqfeq  9805  iseqshft2  9806  iseqsplit  9812  iseqcaopr3  9814  iseqcaopr2  9815  iseqf1olemkle  9817  iseqf1olemklt  9818  iseqf1olemqk  9827  iseqf1olemqsum  9833  iseqf1olemstep  9834  iseqf1olemp  9835  iseqf1oleml  9836  iseqid  9842  iseqid2  9843  iseqhomo  9844  mulexp  9892  expadd  9895  expmul  9898  nn0opth2d  10027  bcpasc  10070  hashennn  10084  hashen  10088  omgadd  10106  hashfzo  10126  hashfzp1  10128  hashxp  10130  hashfacen  10137  iseqcoll  10143  shftvalg  10166  shftval4g  10167  replim  10188  cjreb  10195  cjexp  10222  absexp  10407  recan  10437  sumeq2  10638  zisum  10663  fisum  10665  fsumf1o  10668  moddvds  10680  gcddiv  10883  ialginv  10904  ialgfx  10909  lcmneg  10931  lcmid  10937  lcmgcdeq  10940  divgcdcoprm0  10958  cncongr1  10960  cncongr2  10961  nn0gcdsq  11053  crth  11075  nninfalllemn  11336
  Copyright terms: Public domain W3C validator