Theorem eqeqan12d 2181

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 2178	. 2 |- ( ( A = B /\ C = D ) -> ( A = C <-> B = D ) )
4	1, 2, 3	syl2an 287	1 |- ( ( ph /\ ps ) -> ( A = C <-> B = D ) )

Syntax hints:   -> wi 4   /\ wa 103   <-> wb 104   = wceq 1343

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1435  ax-gen 1437  ax-4 1498  ax-17 1514  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-cleq 2158

This theorem is referenced by:  eqeqan12rd  2182  eqfnfv  5583  eqfnfv2  5584  f1mpt  5739  xpopth  6144  f1o2ndf1  6196  ecopoveq  6596  xpdom2  6797  djune  7043  addpipqqs  7311  enq0enq  7372  enq0sym  7373  enq0tr  7375  enq0breq  7377  preqlu  7413  cnegexlem1  8073  neg11  8149  subeqrev  8274  cnref1o  9588  xneg11  9770  modlteq  10332  sq11  10527  qsqeqor  10565  fz1eqb  10704  cj11  10847  sqrt11  10981  sqabs  11024  recan  11051  reeff1  11641  efieq  11676  tgtop11  12716  ioocosf1o  13415