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

Theorem eqeq12i 2442
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 2429 . 2  |-  ( A  =  C  <->  B  =  C )
3 eqeq12i.2 . . 3  |-  C  =  D
43eqeq2i 2440 . 2  |-  ( B  =  C  <->  B  =  D )
52, 4bitri 252 1  |-  ( A  =  C  <->  B  =  D )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 187    = wceq 1437
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-ext 2401
This theorem depends on definitions:  df-bi 188  df-cleq 2414
This theorem is referenced by:  neeq12i  2709  rabbi  3004  unineq  3723  sbceqg  3803  preqr2  4175  iuneq12df  4323  otth  4703  otthg  4704  rncoeq  5117  sspred  5407  fresaunres1  5773  eqfnov  6416  mpt22eqb  6419  f1o2ndf1  6915  wfrlem5  7051  ecopovsym  7476  karden  8374  adderpqlem  9386  mulerpqlem  9387  addcmpblnr  9500  ax1ne0  9591  addid1  9820  sq11i  12371  nn0opth2i  12463  oppgcntz  17014  islpir  18472  evlsval  18741  volfiniun  22498  dvmptfsum  22925  axlowdimlem13  24982  usgraidx2v  25118  el2wlkonotot0  25598  pjneli  27374  iuneq12daf  28172  madjusmdetlem1  28661  bnj553  29717  bnj1253  29834  frrlem5  30525  sltval2  30550  sltsolem1  30562  altopthsn  30733  bj-2upleq  31574  relowlpssretop  31731  iscrngo2  32195  sbceqi  32312  cdleme18d  33830  fphpd  35628  rp-fakeuninass  36131  relexp0eq  36263  comptiunov2i  36268  onfrALTlem5  36878  onfrALTlem4  36879  onfrALTlem5VD  37255  onfrALTlem4VD  37256  dvnprodlem3  37763  sge0xadd  38185  usgridx2v  39087  issubgr  39116  usgedgvadf1  39346  usgedgvadf1ALT  39349  rabeqsn  39732
  Copyright terms: Public domain W3C validator