Theorem eqeqan12d 2193

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 2190	. 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 1353

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 1447  ax-gen 1449  ax-4 1510  ax-17 1526  ax-ext 2159

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

This theorem is referenced by:  eqeqan12rd  2194  eqfnfv  5615  eqfnfv2  5616  f1mpt  5774  xpopth  6179  f1o2ndf1  6231  ecopoveq  6632  xpdom2  6833  djune  7079  addpipqqs  7371  enq0enq  7432  enq0sym  7433  enq0tr  7435  enq0breq  7437  preqlu  7473  cnegexlem1  8134  neg11  8210  subeqrev  8335  cnref1o  9652  xneg11  9836  modlteq  10399  sq11  10595  qsqeqor  10633  fz1eqb  10772  cj11  10916  sqrt11  11050  sqabs  11093  recan  11120  reeff1  11710  efieq  11745  xpsff1o  12773  ismhm  12858  tgtop11  13661  ioocosf1o  14360