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 1397

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 1495  ax-gen 1497  ax-4 1558  ax-17 1574  ax-ext 2213

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

This theorem is referenced by:  eqeqan12rd  2248  eqfnfv  5744  eqfnfv2  5745  f1mpt  5911  xpopth  6338  f1o2ndf1  6392  ecopoveq  6798  xpdom2  7014  djune  7276  addpipqqs  7589  enq0enq  7650  enq0sym  7651  enq0tr  7653  enq0breq  7655  preqlu  7691  cnegexlem1  8353  neg11  8429  subeqrev  8554  cnref1o  9884  xneg11  10068  modlteq  10658  sq11  10873  qsqeqor  10911  fz1eqb  11051  eqwrd  11153  s111  11207  ccatopth  11296  wrd2ind  11303  cj11  11465  sqrt11  11599  sqabs  11642  recan  11669  reeff1  12260  efieq  12295  xpsff1o  13431  ismhm  13543  isdomn  14282  tgtop11  14799  ioocosf1o  15577  mpodvdsmulf1o  15713  iswlk  16173