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

Theorem eqeq12d 2096
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 2094 . 2 ((𝐴 = 𝐵𝐶 = 𝐷) → (𝐴 = 𝐶𝐵 = 𝐷))
41, 2, 3syl2anc 403 1 (𝜑 → (𝐴 = 𝐶𝐵 = 𝐷))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 103   = wceq 1285
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 1377  ax-gen 1379  ax-4 1441  ax-17 1460  ax-ext 2064
This theorem depends on definitions:  df-bi 115  df-cleq 2075
This theorem is referenced by:  cdeqeq  2811  sbceqg  2923  csbing  3180  uniprg  3624  unisng  3626  intprg  3677  iununir  3767  csbopabg  3864  limeq  4140  onsucuni2  4315  ordpwsucexmid  4321  csbima12g  4716  dmsnsnsng  4828  cnvsng  4836  csbiotag  4925  fvmptf  5295  eqfnfv2f  5301  fvreseq  5303  fmptco  5362  fnressn  5381  fvsng  5391  cocan1  5458  cocan2  5459  fliftfun  5467  csbriotag  5511  csbov123g  5574  eqfnov  5638  ovmpt2s  5655  ov2gf  5656  ovmpt2dxf  5657  caovcomg  5687  caovassg  5690  caovcang  5693  caovcanrd  5695  caovcan  5696  caovdig  5706  caovdirg  5709  caovimo  5725  grprinvlem  5726  grprinvd  5727  offveqb  5761  op1stg  5808  op2ndg  5809  f1o2ndf1  5880  tfrlem1  5957  tfrlem3ag  5958  tfrlem3a  5959  tfrlem5  5963  tfrlem9  5968  tfr0dm  5971  tfrlemiubacc  5979  tfrlemiex  5980  tfrlemi1  5981  tfr1onlem3ag  5986  tfr1onlemubacc  5995  tfr1onlemex  5996  tfr1onlemaccex  5997  tfrcllemsucaccv  6003  tfrcllembxssdm  6005  tfrcllemubacc  6008  tfrcllemex  6009  tfrcllemaccex  6010  tfrcllemres  6011  tfrcldm  6012  tfri3  6016  rdg0g  6037  frecrdg  6057  nna0r  6122  nnacom  6128  nnaass  6129  nndi  6130  nnmass  6131  nnmsucr  6132  nnmcom  6133  ecopovtrn  6269  ecopovsymg  6271  ecopovtrng  6272  ecovcom  6279  ecovicom  6280  ecovass  6281  ecoviass  6282  ecovdi  6283  ecovidi  6284  dom2lem  6319  ordiso2  6505  addcanpig  6586  mulcanpig  6587  mulcmpblnq  6620  mulpipqqs  6625  ordpipqqs  6626  mulidnq  6641  enq0sym  6684  nqnq0  6693  mulcmpblnq0  6696  distrnq0  6711  mulcomnq0  6712  addassnq0  6714  nq02m  6717  genipv  6761  cauappcvgprlemladd  6910  addcmpblnr  6978  0idsr  7006  1idsr  7007  axaddcom  7098  ax1rid  7105  ax0id  7106  rereceu  7117  axcaucvg  7128  mulid1  7178  readdcan  7315  cnegexlem1  7350  cnegexlem3  7352  addcan  7355  addcan2  7356  apti  7789  mulcanapd  7818  mulcanap2d  7819  div11ap  7855  divmuleqap  7872  conjmulap  7884  eqneg  7887  cnref1o  8814  fzsuc2  9172  fzprval  9175  fztpval  9176  qtri3or  9329  modqadd1  9443  modqmul1  9459  addmodlteq  9480  frec2uzrdg  9491  frecuzrdgg  9498  iseqvalt  9532  iseqoveq  9540  iseqss  9541  iseqsst  9542  iseqfveq2  9544  iseqfveq  9546  iseqfeq  9547  iseqshft2  9548  iseqsplit  9554  iseqcaopr3  9556  iseqcaopr2  9557  iseqid  9563  iseqid2  9564  iseqhomo  9565  mulexp  9612  expadd  9615  expmul  9618  nn0opth2d  9747  bcpasc  9790  sizeennn  9804  sizeen  9808  omgadd  9826  shftvalg  9862  shftval4g  9863  replim  9884  cjreb  9891  cjexp  9918  absexp  10103  recan  10133  sumeq2d  10334  sumeq2  10335  moddvds  10349  gcddiv  10552  ialginv  10573  ialgfx  10578  lcmneg  10600  lcmid  10606  lcmgcdeq  10609  divgcdcoprm0  10627  cncongr1  10629  cncongr2  10630  nn0gcdsq  10722
  Copyright terms: Public domain W3C validator