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  5614  eqfnfv2  5615  f1mpt  5772  xpopth  6177  f1o2ndf1  6229  ecopoveq  6630  xpdom2  6831  djune  7077  addpipqqs  7369  enq0enq  7430  enq0sym  7431  enq0tr  7433  enq0breq  7435  preqlu  7471  cnegexlem1  8132  neg11  8208  subeqrev  8333  cnref1o  9650  xneg11  9834  modlteq  10397  sq11  10593  qsqeqor  10631  fz1eqb  10770  cj11  10914  sqrt11  11048  sqabs  11091  recan  11118  reeff1  11708  efieq  11743  xpsff1o  12768  ismhm  12853  tgtop11  13579  ioocosf1o  14278