Theorem eqeqan12d 2254

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 2251	. 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 1402

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 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

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

This theorem is referenced by:  eqeqan12rd  2255  eqfnfv  5797  eqfnfv2  5798  f1mpt  5967  xpopth  6400  f1o2ndf1  6454  ecopoveq  6894  xpdom2  7119  djune  7408  addpipqqs  7727  enq0enq  7788  enq0sym  7789  enq0tr  7791  enq0breq  7793  preqlu  7829  cnegexlem1  8491  neg11  8567  subeqrev  8692  cnref1o  10030  xneg11  10215  modlteq  10812  sq11  11027  qsqeqor  11065  fz1eqb  11207  eqwrd  11323  s111  11377  ccatopth  11466  wrd2ind  11473  cj11  11649  sqrt11  11783  sqabs  11826  recan  11853  reeff1  12445  efieq  12480  xpsff1o  13647  ismhm  13745  isdomn  14551  tgtop11  15100  ioocosf1o  15878  mpodvdsmulf1o  16018  iswlk  16478