Theorem eqeqan12d 2248

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 2245	. 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 1398

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575  ax-ext 2214

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

This theorem is referenced by:  eqeqan12rd  2249  eqfnfv  5775  eqfnfv2  5776  f1mpt  5944  xpopth  6370  f1o2ndf1  6424  ecopoveq  6864  xpdom2  7082  djune  7369  addpipqqs  7685  enq0enq  7746  enq0sym  7747  enq0tr  7749  enq0breq  7751  preqlu  7787  cnegexlem1  8448  neg11  8524  subeqrev  8649  cnref1o  9983  xneg11  10167  modlteq  10759  sq11  10974  qsqeqor  11012  fz1eqb  11153  eqwrd  11265  s111  11319  ccatopth  11408  wrd2ind  11415  cj11  11590  sqrt11  11724  sqabs  11767  recan  11794  reeff1  12386  efieq  12421  xpsff1o  13562  ismhm  13674  isdomn  14415  tgtop11  14941  ioocosf1o  15719  mpodvdsmulf1o  15858  iswlk  16318