Theorem eqeqan12d 2096

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

Step	Hyp	Ref	Expression
1		eqeqan12d.1	. 2 |- ( ph -> A = B )
2		eqeqan12d.2	. 2 |- ( ps -> C = D )
3		eqeq12 2093	. 2 |- ( ( A = B /\ C = D ) -> ( A = C <-> B = D ) )
4	1, 2, 3	syl2an 283	1 |- ( ( ph /\ ps ) -> ( A = C <-> B = D ) )

Syntax hints:   -> wi 4   /\ wa 102   <-> wb 103   = wceq 1284

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1376  ax-gen 1378  ax-4 1440  ax-17 1459  ax-ext 2063

This theorem depends on definitions:  df-bi 115  df-cleq 2074

This theorem is referenced by:  eqeqan12rd  2097  eqfnfv  5286  eqfnfv2  5287  f1mpt  5431  xpopth  5822  f1o2ndf1  5869  ecopoveq  6224  xpdom2  6328  addpipqqs  6560  enq0enq  6621  enq0sym  6622  enq0tr  6624  enq0breq  6626  preqlu  6662  cnegexlem1  7283  neg11  7359  subeqrev  7480  cnref1o  8733  xneg11  8901  modlteq  9399  sq11  9548  cj11  9792  sqrt11  9925  sqabs  9968  recan  9995