Theorem eqeqan12d 2220

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 2217	. 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 1372

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 1469  ax-gen 1471  ax-4 1532  ax-17 1548  ax-ext 2186

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

This theorem is referenced by:  eqeqan12rd  2221  eqfnfv  5676  eqfnfv2  5677  f1mpt  5839  xpopth  6261  f1o2ndf1  6313  ecopoveq  6716  xpdom2  6925  djune  7179  addpipqqs  7482  enq0enq  7543  enq0sym  7544  enq0tr  7546  enq0breq  7548  preqlu  7584  cnegexlem1  8246  neg11  8322  subeqrev  8447  cnref1o  9771  xneg11  9955  modlteq  10540  sq11  10755  qsqeqor  10793  fz1eqb  10933  eqwrd  11032  s111  11083  cj11  11187  sqrt11  11321  sqabs  11364  recan  11391  reeff1  11982  efieq  12017  xpsff1o  13152  ismhm  13264  isdomn  14002  tgtop11  14519  ioocosf1o  15297  mpodvdsmulf1o  15433