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

Theorem eqeq12i 2448
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 2447 . 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 1652
This theorem is referenced by:  rabbi  2878  sbceqg  3259  unineq  3583  preqr2  3965  otth  4432  rncoeq  5131  fresaunres1  5608  eqfnov  6168  mpt22eqb  6171  f1o2ndf1  6446  ecopovsym  6998  karden  7811  adderpqlem  8823  mulerpqlem  8824  addcmpblnr  8939  ax1ne0  9027  addid1  9238  sq11i  11464  nn0opth2i  11556  oppgcntz  15152  islpir  16312  volfiniun  19433  dvmptfsum  19851  evlsval  19932  usgraidx2v  21404  pjneli  23217  iuneq12daf  23999  iuneq12df  24000  sspred  25439  wfrlem5  25534  frrlem5  25578  sltval2  25603  sltsolem1  25615  altopthsn  25798  axlowdimlem13  25885  iscrngo2  26589  fphpd  26858  otthg  28044  el2wlkonotot0  28282  onfrALTlem5  28555  onfrALTlem4  28556  onfrALTlem5VD  28924  onfrALTlem4VD  28925  bnj553  29196  bnj1253  29313  cdleme18d  31019
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-11 1761  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1551  df-cleq 2428
  Copyright terms: Public domain W3C validator