Theorem eqeqan12d 2212

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 2209	. 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 1461  ax-gen 1463  ax-4 1524  ax-17 1540  ax-ext 2178

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

This theorem is referenced by:  eqeqan12rd  2213  eqfnfv  5662  eqfnfv2  5663  f1mpt  5821  xpopth  6243  f1o2ndf1  6295  ecopoveq  6698  xpdom2  6899  djune  7153  addpipqqs  7456  enq0enq  7517  enq0sym  7518  enq0tr  7520  enq0breq  7522  preqlu  7558  cnegexlem1  8220  neg11  8296  subeqrev  8421  cnref1o  9744  xneg11  9928  modlteq  10508  sq11  10723  qsqeqor  10761  fz1eqb  10901  eqwrd  10994  cj11  11089  sqrt11  11223  sqabs  11266  recan  11293  reeff1  11884  efieq  11919  xpsff1o  13053  ismhm  13165  isdomn  13903  tgtop11  14420  ioocosf1o  15198  mpodvdsmulf1o  15334