Theorem eqeqan12d 2247

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

Syntax hints:   -> wi 4   /\ wa 104   <-> wb 105   = wceq 1398

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-cleq 2224

This theorem is referenced by:  eqeqan12rd  2248  eqfnfv  5753  eqfnfv2  5754  f1mpt  5922  xpopth  6348  f1o2ndf1  6402  ecopoveq  6842  xpdom2  7058  djune  7320  addpipqqs  7633  enq0enq  7694  enq0sym  7695  enq0tr  7697  enq0breq  7699  preqlu  7735  cnegexlem1  8396  neg11  8472  subeqrev  8597  cnref1o  9929  xneg11  10113  modlteq  10705  sq11  10920  qsqeqor  10958  fz1eqb  11098  eqwrd  11203  s111  11257  ccatopth  11346  wrd2ind  11353  cj11  11528  sqrt11  11662  sqabs  11705  recan  11732  reeff1  12324  efieq  12359  xpsff1o  13495  ismhm  13607  isdomn  14348  tgtop11  14870  ioocosf1o  15648  mpodvdsmulf1o  15787  iswlk  16247