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

Theorem eqeq12i 2296
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  =  C  <->  B  =  D )

Proof of Theorem eqeq12i
StepHypRef Expression
1 eqeq12i.1 . 2  |-  A  =  B
2 eqeq12i.2 . 2  |-  C  =  D
3 eqeq12 2295 . 2  |-  ( ( A  =  B  /\  C  =  D )  ->  ( A  =  C  <-> 
B  =  D ) )
41, 2, 3mp2an 653 1  |-  ( A  =  C  <->  B  =  D )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    = wceq 1623
This theorem is referenced by:  rabbi  2718  sbceqg  3097  unineq  3419  preqr2  3787  otth  4250  rncoeq  4948  fresaunres1  5414  eqfnov  5950  mpt22eqb  5953  ecopovsym  6760  karden  7565  adderpqlem  8578  mulerpqlem  8579  addcmpblnr  8694  ax1ne0  8782  addid1  8992  sq11i  11194  nn0opth2i  11286  oppgcntz  14837  islpir  16001  volfiniun  18904  dvmptfsum  19322  evlsval  19403  pjneli  22302  iuneq12daf  23154  iuneq12df  23155  sspred  24174  wfrlem5  24260  frrlem5  24285  sltval2  24310  sltsolem1  24322  altopthsn  24495  axlowdimlem13  24582  trooo  25394  vecval3b  25452  cnegvex2b  25662  rnegvex2b  25663  addcanrg  25667  dualcat2  25784  ismona  25809  issrc  25867  propsrc  25868  isntr  25873  cmp2morpcats  25961  iscrngo2  26623  fphpd  26899  compneOLD  27643  onfrALTlem5  28307  onfrALTlem4  28308  onfrALTlem5VD  28661  onfrALTlem4VD  28662  bnj553  28930  bnj1253  29047  cdleme18d  30484
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-11 1715  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-cleq 2276
  Copyright terms: Public domain W3C validator