ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  eqeqan12d Unicode version

Theorem eqeqan12d 2220
Description: A useful inference for substituting definitions into an equality. (Contributed by NM, 9-Aug-1994.) (Proof shortened by Andrew Salmon, 25-May-2011.)
Hypotheses
Ref Expression
eqeqan12d.1  |-  ( ph  ->  A  =  B )
eqeqan12d.2  |-  ( ps 
->  C  =  D
)
Assertion
Ref Expression
eqeqan12d  |-  ( (
ph  /\  ps )  ->  ( A  =  C  <-> 
B  =  D ) )

Proof of Theorem eqeqan12d
StepHypRef Expression
1 eqeqan12d.1 . 2  |-  ( ph  ->  A  =  B )
2 eqeqan12d.2 . 2  |-  ( ps 
->  C  =  D
)
3 eqeq12 2217 . 2  |-  ( ( A  =  B  /\  C  =  D )  ->  ( A  =  C  <-> 
B  =  D ) )
41, 2, 3syl2an 289 1  |-  ( (
ph  /\  ps )  ->  ( A  =  C  <-> 
B  =  D ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 104    <-> wb 105    = wceq 1372
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1469  ax-gen 1471  ax-4 1532  ax-17 1548  ax-ext 2186
This theorem depends on definitions:  df-bi 117  df-cleq 2197
This theorem is referenced by:  eqeqan12rd  2221  eqfnfv  5676  eqfnfv2  5677  f1mpt  5839  xpopth  6261  f1o2ndf1  6313  ecopoveq  6716  xpdom2  6925  djune  7179  addpipqqs  7482  enq0enq  7543  enq0sym  7544  enq0tr  7546  enq0breq  7548  preqlu  7584  cnegexlem1  8246  neg11  8322  subeqrev  8447  cnref1o  9771  xneg11  9955  modlteq  10540  sq11  10755  qsqeqor  10793  fz1eqb  10933  eqwrd  11032  s111  11083  cj11  11187  sqrt11  11321  sqabs  11364  recan  11391  reeff1  11982  efieq  12017  xpsff1o  13152  ismhm  13264  isdomn  14002  tgtop11  14519  ioocosf1o  15297  mpodvdsmulf1o  15433
  Copyright terms: Public domain W3C validator