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

Theorem eqeq12i 2402
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 2401 . 2  |-  ( ( A  =  B  /\  C  =  D )  ->  ( A  =  C  <-> 
B  =  D ) )
41, 2, 3mp2an 654 1  |-  ( A  =  C  <->  B  =  D )
Colors of variables: wff set class
Syntax hints:    <-> wb 177    = wceq 1649
This theorem is referenced by:  rabbi  2831  sbceqg  3212  unineq  3536  preqr2  3917  otth  4383  rncoeq  5081  fresaunres1  5558  eqfnov  6117  mpt22eqb  6120  ecopovsym  6944  karden  7754  adderpqlem  8766  mulerpqlem  8767  addcmpblnr  8882  ax1ne0  8970  addid1  9180  sq11i  11401  nn0opth2i  11493  oppgcntz  15089  islpir  16249  volfiniun  19310  dvmptfsum  19728  evlsval  19809  usgraidx2v  21280  pjneli  23075  iuneq12daf  23853  iuneq12df  23854  sspred  25200  wfrlem5  25286  frrlem5  25311  sltval2  25336  sltsolem1  25348  altopthsn  25522  axlowdimlem13  25609  iscrngo2  26301  fphpd  26570  onfrALTlem5  27973  onfrALTlem4  27974  onfrALTlem5VD  28340  onfrALTlem4VD  28341  bnj553  28609  bnj1253  28726  cdleme18d  30411
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-11 1753  ax-ext 2370
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-cleq 2382
  Copyright terms: Public domain W3C validator