Theorem eqeqan12d 2223

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 2220	. 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 1373

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 1471  ax-gen 1473  ax-4 1534  ax-17 1550  ax-ext 2189

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

This theorem is referenced by:  eqeqan12rd  2224  eqfnfv  5700  eqfnfv2  5701  f1mpt  5863  xpopth  6285  f1o2ndf1  6337  ecopoveq  6740  xpdom2  6951  djune  7206  addpipqqs  7518  enq0enq  7579  enq0sym  7580  enq0tr  7582  enq0breq  7584  preqlu  7620  cnegexlem1  8282  neg11  8358  subeqrev  8483  cnref1o  9807  xneg11  9991  modlteq  10579  sq11  10794  qsqeqor  10832  fz1eqb  10972  eqwrd  11071  s111  11123  ccatopth  11207  wrd2ind  11214  cj11  11331  sqrt11  11465  sqabs  11508  recan  11535  reeff1  12126  efieq  12161  xpsff1o  13296  ismhm  13408  isdomn  14146  tgtop11  14663  ioocosf1o  15441  mpodvdsmulf1o  15577