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

Theorem eqeqan12d 2153
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 2150 . 2  |-  ( ( A  =  B  /\  C  =  D )  ->  ( A  =  C  <-> 
B  =  D ) )
41, 2, 3syl2an 287 1  |-  ( (
ph  /\  ps )  ->  ( A  =  C  <-> 
B  =  D ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103    <-> wb 104    = wceq 1331
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-gen 1425  ax-4 1487  ax-17 1506  ax-ext 2119
This theorem depends on definitions:  df-bi 116  df-cleq 2130
This theorem is referenced by:  eqeqan12rd  2154  eqfnfv  5511  eqfnfv2  5512  f1mpt  5665  xpopth  6067  f1o2ndf1  6118  ecopoveq  6517  xpdom2  6718  djune  6956  addpipqqs  7171  enq0enq  7232  enq0sym  7233  enq0tr  7235  enq0breq  7237  preqlu  7273  cnegexlem1  7930  neg11  8006  subeqrev  8131  cnref1o  9433  xneg11  9610  modlteq  10163  sq11  10358  fz1eqb  10530  cj11  10670  sqrt11  10804  sqabs  10847  recan  10874  reeff1  11392  efieq  11427  tgtop11  12230
  Copyright terms: Public domain W3C validator