MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  eqeq12i Structured version   Visualization version   GIF version

Theorem eqeq12i 2751
Description: A useful inference for substituting definitions into an equality. (Contributed by NM, 15-Jul-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 20-Nov-2019.)
Hypotheses
Ref Expression
eqeq12i.1 𝐴 = 𝐵
eqeq12i.2 𝐶 = 𝐷
Assertion
Ref Expression
eqeq12i (𝐴 = 𝐶𝐵 = 𝐷)

Proof of Theorem eqeq12i
StepHypRef Expression
1 eqeq12i.1 . . 3 𝐴 = 𝐵
21eqeq1i 2738 . 2 (𝐴 = 𝐶𝐵 = 𝐶)
3 eqeq12i.2 . . 3 𝐶 = 𝐷
43eqeq2i 2746 . 2 (𝐵 = 𝐶𝐵 = 𝐷)
52, 4bitri 275 1 (𝐴 = 𝐶𝐵 = 𝐷)
Colors of variables: wff setvar class
Syntax hints:  wb 205   = wceq 1542
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725
This theorem is referenced by:  neeq12i  3007  rabbi  3431  unineq  4241  vn0  4302  sbceqg  4373  sbceqi  4374  preq2b  4809  preqr2  4811  otth  5445  otthg  5446  rncoeq  5934  fresaunres1  6719  eqfnov  7489  mpo2eqb  7492  f1o2ndf1  8058  fprlem1  8235  wfrlem5OLD  8263  ecopovsym  8764  frrlem15  9701  karden  9839  adderpqlem  10898  mulerpqlem  10899  addcmpblnr  11013  ax1ne0  11104  addrid  11343  sq11i  14104  nn0opth2i  14180  oppgcntz  19153  islpir  20764  evlsval  21519  volfiniun  24934  dvmptfsum  25362  sltval2  27027  sltsolem1  27046  nosepnelem  27050  nolt02o  27066  axlowdimlem13  27952  usgredg2v  28224  issubgr  28268  clwlkcompbp  28779  pjneli  30714  indifbi  31497  madjusmdetlem1  32472  breprexp  33310  bnj553  33574  bnj1253  33693  gonanegoal  34010  goalrlem  34054  goalr  34055  fmlasucdisj  34057  satffunlem  34059  satffunlem1lem1  34060  satffunlem2lem1  34062  altopthsn  34599  bj-2upleq  35533  relowlpssretop  35885  iscrngo2  36506  extid  36821  cdleme18d  38808  fphpd  41186  oenassex  41700  rp-fakeuninass  41880  relexp0eq  42065  comptiunov2i  42070  clsk1indlem1  42409  ntrclskb  42433  onfrALTlem5  42916  onfrALTlem4  42917  onfrALTlem5VD  43259  onfrALTlem4VD  43260  dvnprodlem3  44279  sge0xadd  44766  reuabaiotaiota  45409  rrx2linest  46918
  Copyright terms: Public domain W3C validator