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

Theorem eqeq12d 2367
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
eqeq12d.1 (φA = B)
eqeq12d.2 (φC = D)
Assertion
Ref Expression
eqeq12d (φ → (A = CB = D))

Proof of Theorem eqeq12d
StepHypRef Expression
1 eqeq12d.1 . 2 (φA = B)
2 eqeq12d.2 . 2 (φC = D)
3 eqeq12 2365 . 2 ((A = B C = D) → (A = CB = D))
41, 2, 3syl2anc 642 1 (φ → (A = CB = D))
Colors of variables: wff setvar class
Syntax hints:  wi 4  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:  sbceqg  3152  csbing  3462  csbifg  3690  uniprg  3906  unisng  3908  intprg  3960  iununi  4050  csbiotag  4371  preaddccan2  4455  csbopabg  4637  csbima12g  4955  fveqres  5355  eqfnfv2f  5396  fvreseq  5398  fnressn  5438  fvi  5442  fvsng  5446  csbovg  5552  eqfnov  5589  ov2ag  5598  caovcomg  5624  caovassg  5626  caovcan  5628  caovdig  5632  caovdirg  5633  caovmo  5645  ov2gf  5711  fvmptf  5722  fvfullfun  5864  taddc  6229  letc  6231  addcdi  6250  addccan2nc  6265  nchoicelem1  6289  nchoicelem2  6290  nchoicelem9  6297  nchoicelem17  6305  nchoice  6308
  Copyright terms: Public domain W3C validator