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

Theorem eqeq12i 2474
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  |-  A  =  B
eqeq12i.2  |-  C  =  D
Assertion
Ref Expression
eqeq12i  |-  ( A  =  C  <->  B  =  D )

Proof of Theorem eqeq12i
StepHypRef Expression
1 eqeq12i.1 . . 3  |-  A  =  B
21eqeq1i 2461 . 2  |-  ( A  =  C  <->  B  =  C )
3 eqeq12i.2 . . 3  |-  C  =  D
43eqeq2i 2472 . 2  |-  ( B  =  C  <->  B  =  D )
52, 4bitri 249 1  |-  ( A  =  C  <->  B  =  D )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    = wceq 1370
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-cleq 2446
This theorem is referenced by:  neeq12i  2741  rabbi  3005  csbeq2  3402  unineq  3711  sbceqg  3788  preqr2  4158  iuneq12df  4305  otth  4685  rncoeq  5214  fresaunres1  5695  eqfnov  6309  mpt22eqb  6312  f1o2ndf1  6793  ecopovsym  7315  karden  8216  adderpqlem  9237  mulerpqlem  9238  addcmpblnr  9353  ax1ne0  9441  addid1  9663  sq11i  12076  nn0opth2i  12169  oppgcntz  16001  islpir  17457  evlsval  17732  volfiniun  21164  dvmptfsum  21583  axlowdimlem13  23372  usgraidx2v  23483  pjneli  25298  iuneq12daf  26079  gsumvsca1  26416  gsumvsca2  26417  sspred  27797  wfrlem5  27892  frrlem5  27936  sltval2  27961  sltsolem1  27973  altopthsn  28156  iscrngo2  28966  sbceqi  29084  fphpd  29323  otthg  30298  el2wlkonotot0  30559  rabeqsn  30885  onfrALTlem5  31602  onfrALTlem4  31603  onfrALTlem5VD  31973  onfrALTlem4VD  31974  bnj553  32243  bnj1253  32360  bj-2upleq  32857  cdleme18d  34297
  Copyright terms: Public domain W3C validator