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

Theorem eqeqan12d 2193
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 2190 . 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 1353
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 1447  ax-gen 1449  ax-4 1510  ax-17 1526  ax-ext 2159
This theorem depends on definitions:  df-bi 117  df-cleq 2170
This theorem is referenced by:  eqeqan12rd  2194  eqfnfv  5613  eqfnfv2  5614  f1mpt  5771  xpopth  6176  f1o2ndf1  6228  ecopoveq  6629  xpdom2  6830  djune  7076  addpipqqs  7368  enq0enq  7429  enq0sym  7430  enq0tr  7432  enq0breq  7434  preqlu  7470  cnegexlem1  8131  neg11  8207  subeqrev  8332  cnref1o  9649  xneg11  9833  modlteq  10396  sq11  10592  qsqeqor  10630  fz1eqb  10769  cj11  10913  sqrt11  11047  sqabs  11090  recan  11117  reeff1  11707  efieq  11742  xpsff1o  12767  ismhm  12852  tgtop11  13546  ioocosf1o  14245
  Copyright terms: Public domain W3C validator