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

Theorem eqeq12i 2309
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 2308 . 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 1632
This theorem is referenced by:  rabbi  2731  sbceqg  3110  unineq  3432  preqr2  3803  otth  4266  rncoeq  4964  fresaunres1  5430  eqfnov  5966  mpt22eqb  5969  ecopovsym  6776  karden  7581  adderpqlem  8594  mulerpqlem  8595  addcmpblnr  8710  ax1ne0  8798  addid1  9008  sq11i  11210  nn0opth2i  11302  oppgcntz  14853  islpir  16017  volfiniun  18920  dvmptfsum  19338  evlsval  19419  pjneli  22318  iuneq12daf  23170  iuneq12df  23171  sspred  24245  wfrlem5  24331  frrlem5  24356  sltval2  24381  sltsolem1  24393  altopthsn  24567  axlowdimlem13  24654  trooo  25497  vecval3b  25555  cnegvex2b  25765  rnegvex2b  25766  addcanrg  25770  dualcat2  25887  ismona  25912  issrc  25970  propsrc  25971  isntr  25976  cmp2morpcats  26064  iscrngo2  26726  fphpd  27002  compneOLD  27746  onfrALTlem5  28606  onfrALTlem4  28607  onfrALTlem5VD  28977  onfrALTlem4VD  28978  bnj553  29246  bnj1253  29363  cdleme18d  31106
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-11 1727  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-an 360  df-cleq 2289
  Copyright terms: Public domain W3C validator