Theorem eqeqan12d 2209

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 2206	. 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 1364

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 1458  ax-gen 1460  ax-4 1521  ax-17 1537  ax-ext 2175

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

This theorem is referenced by:  eqeqan12rd  2210  eqfnfv  5655  eqfnfv2  5656  f1mpt  5814  xpopth  6229  f1o2ndf1  6281  ecopoveq  6684  xpdom2  6885  djune  7137  addpipqqs  7430  enq0enq  7491  enq0sym  7492  enq0tr  7494  enq0breq  7496  preqlu  7532  cnegexlem1  8194  neg11  8270  subeqrev  8395  cnref1o  9716  xneg11  9900  modlteq  10468  sq11  10683  qsqeqor  10721  fz1eqb  10861  eqwrd  10954  cj11  11049  sqrt11  11183  sqabs  11226  recan  11253  reeff1  11843  efieq  11878  xpsff1o  12932  ismhm  13033  isdomn  13765  tgtop11  14244  ioocosf1o  14989