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

Theorem eqeq12i 2813
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 2803 . 2 (𝐴 = 𝐶𝐵 = 𝐶)
3 eqeq12i.2 . . 3 𝐶 = 𝐷
43eqeq2i 2811 . 2 (𝐵 = 𝐶𝐵 = 𝐷)
52, 4bitri 278 1 (𝐴 = 𝐶𝐵 = 𝐷)
Colors of variables: wff setvar class
Syntax hints:  wb 209   = wceq 1538
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2121  ax-ext 2770
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2791
This theorem is referenced by:  neeq12i  3053  rabbi  3336  unineq  4204  sbceqg  4317  sbceqi  4318  preq2b  4738  preqr2  4740  otth  5341  otthg  5342  rncoeq  5811  fresaunres1  6525  eqfnov  7259  mpo2eqb  7262  f1o2ndf1  7801  wfrlem5  7942  ecopovsym  8382  karden  9308  adderpqlem  10365  mulerpqlem  10366  addcmpblnr  10480  ax1ne0  10571  addid1  10809  sq11i  13550  nn0opth2i  13627  oppgcntz  18484  islpir  20015  evlsval  20758  volfiniun  24151  dvmptfsum  24578  axlowdimlem13  26748  usgredg2v  27017  issubgr  27061  clwlkcompbp  27571  pjneli  29506  indifbi  30292  madjusmdetlem1  31180  breprexp  32014  bnj553  32280  bnj1253  32399  gonanegoal  32709  goalrlem  32753  goalr  32754  fmlasucdisj  32756  satffunlem  32758  satffunlem1lem1  32759  satffunlem2lem1  32761  fprlem1  33247  frrlem15  33252  sltval2  33273  sltsolem1  33290  nosepnelem  33294  nolt02o  33309  altopthsn  33532  bj-2upleq  34445  relowlpssretop  34778  iscrngo2  35432  extid  35725  cdleme18d  37588  fphpd  39752  rp-fakeuninass  40219  relexp0eq  40397  comptiunov2i  40402  clsk1indlem1  40743  ntrclskb  40767  onfrALTlem5  41243  onfrALTlem4  41244  onfrALTlem5VD  41586  onfrALTlem4VD  41587  dvnprodlem3  42585  sge0xadd  43069  reuabaiotaiota  43639  rrx2linest  45151
  Copyright terms: Public domain W3C validator