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

Theorem eqeq12i 2624
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 2615 . 2 (𝐴 = 𝐶𝐵 = 𝐶)
3 eqeq12i.2 . . 3 𝐶 = 𝐷
43eqeq2i 2622 . 2 (𝐵 = 𝐶𝐵 = 𝐷)
52, 4bitri 263 1 (𝐴 = 𝐶𝐵 = 𝐷)
Colors of variables: wff setvar class
Syntax hints:  wb 195   = wceq 1475
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-cleq 2603
This theorem is referenced by:  neeq12i  2848  rabbi  3097  unineq  3836  sbceqg  3936  rabeqsn  4161  preq2b  4318  preqr2  4321  iuneq12df  4480  otth  4879  otthg  4880  rncoeq  5310  fresaunres1  5990  eqfnov  6664  mpt22eqb  6667  f1o2ndf1  7172  wfrlem5  7306  ecopovsym  7736  karden  8641  adderpqlem  9655  mulerpqlem  9656  addcmpblnr  9769  ax1ne0  9860  addid1  10095  sq11i  12816  nn0opth2i  12920  oppgcntz  17617  islpir  19070  evlsval  19340  volfiniun  23122  dvmptfsum  23542  axlowdimlem13  25634  usgraidx2v  25922  el2wlkonotot0  26399  pjneli  27966  iuneq12daf  28756  madjusmdetlem1  29221  bnj553  30222  bnj1253  30339  frrlem5  31028  sltval2  31053  sltsolem1  31067  altopthsn  31238  bj-2upleq  32193  relowlpssretop  32388  iscrngo2  32966  sbceqi  33083  cdleme18d  34600  fphpd  36398  rp-fakeuninass  36881  relexp0eq  37012  comptiunov2i  37017  clsk1indlem1  37363  ntrclskb  37387  onfrALTlem5  37778  onfrALTlem4  37779  onfrALTlem5VD  38143  onfrALTlem4VD  38144  dvnprodlem3  38838  sge0xadd  39328  usgredg2v  40454  issubgr  40495
  Copyright terms: Public domain W3C validator