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

Theorem eqeq12i 2476
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 2467 . 2  |-  ( A  =  C  <->  B  =  C )
3 eqeq12i.2 . . 3  |-  C  =  D
43eqeq2i 2474 . 2  |-  ( B  =  C  <->  B  =  D )
52, 4bitri 257 1  |-  ( A  =  C  <->  B  =  D )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 189    = wceq 1455
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-ext 2442
This theorem depends on definitions:  df-bi 190  df-cleq 2455
This theorem is referenced by:  neeq12i  2702  rabbi  2981  unineq  3705  sbceqg  3785  rabeqsn  4013  preq2b  4160  preqr2  4163  iuneq12df  4316  otth  4701  otthg  4702  rncoeq  5120  sspred  5411  fresaunres1  5783  eqfnov  6434  mpt22eqb  6437  f1o2ndf1  6936  wfrlem5  7071  ecopovsym  7496  karden  8397  adderpqlem  9410  mulerpqlem  9411  addcmpblnr  9524  ax1ne0  9615  addid1  9844  sq11i  12403  nn0opth2i  12495  oppgcntz  17070  islpir  18528  evlsval  18797  volfiniun  22556  dvmptfsum  22983  axlowdimlem13  25040  usgraidx2v  25176  el2wlkonotot0  25656  pjneli  27432  iuneq12daf  28225  madjusmdetlem1  28704  bnj553  29759  bnj1253  29876  frrlem5  30568  sltval2  30593  sltsolem1  30607  altopthsn  30778  bj-2upleq  31652  relowlpssretop  31813  iscrngo2  32277  sbceqi  32394  cdleme18d  33907  fphpd  35705  rp-fakeuninass  36207  relexp0eq  36339  comptiunov2i  36344  onfrALTlem5  36953  onfrALTlem4  36954  onfrALTlem5VD  37323  onfrALTlem4VD  37324  dvnprodlem3  37909  sge0xadd  38380  usgredg2v  39450  issubgr  39489  usgedgvadf1  40096  usgedgvadf1ALT  40099
  Copyright terms: Public domain W3C validator