Theorem eqeqan12d 2156

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 2153	. 2 |- ( ( A = B /\ C = D ) -> ( A = C <-> B = D ) )
4	1, 2, 3	syl2an 287	1 |- ( ( ph /\ ps ) -> ( A = C <-> B = D ) )

Syntax hints:   -> wi 4   /\ wa 103   <-> wb 104   = wceq 1332

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 1424  ax-gen 1426  ax-4 1488  ax-17 1507  ax-ext 2122

This theorem depends on definitions:  df-bi 116  df-cleq 2133

This theorem is referenced by:  eqeqan12rd  2157  eqfnfv  5526  eqfnfv2  5527  f1mpt  5680  xpopth  6082  f1o2ndf1  6133  ecopoveq  6532  xpdom2  6733  djune  6971  addpipqqs  7202  enq0enq  7263  enq0sym  7264  enq0tr  7266  enq0breq  7268  preqlu  7304  cnegexlem1  7961  neg11  8037  subeqrev  8162  cnref1o  9469  xneg11  9647  modlteq  10201  sq11  10396  fz1eqb  10569  cj11  10709  sqrt11  10843  sqabs  10886  recan  10913  reeff1  11443  efieq  11478  tgtop11  12284  ioocosf1o  12983