New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  eqeq12i GIF version

Theorem eqeq12i 2366
 Description: A useful inference for substituting definitions into an equality. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.)
Hypotheses
Ref Expression
eqeq12i.1 A = B
eqeq12i.2 C = D
Assertion
Ref Expression
eqeq12i (A = CB = D)

Proof of Theorem eqeq12i
StepHypRef Expression
1 eqeq12i.1 . 2 A = B
2 eqeq12i.2 . 2 C = D
3 eqeq12 2365 . 2 ((A = B C = D) → (A = CB = D))
41, 2, 3mp2an 653 1 (A = CB = D)
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 176   = wceq 1642 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-11 1746  ax-ext 2334 This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1542  df-cleq 2346 This theorem is referenced by:  rabbi  2789  sbceqg  3152  unineq  3505  preqr2  4125  opkthg  4131  preaddccan2  4455  ltfinirr  4457  addccan1  4560  rncoeq  4975  swapf1o  5511  eqfnov  5589  eqncg  6126  ncseqnc  6128  tc11  6228  taddc  6229  muc0or  6252  addccan2nc  6265  nnc3n3p1  6278
 Copyright terms: Public domain W3C validator