Theorem eqeqan12d 2254

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

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   <-> wb 105   = wceq 1402

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231

This theorem is used by:  eqeqan12rd  2255  eqfnfv  5809  eqfnfv2  5810  f1mpt  5980  xpopth  6414  f1o2ndf1  6468  ecopoveq  6909  xpdom2  7135  djune  7424  addpipqqs  7743  enq0enq  7804  enq0sym  7805  enq0tr  7807  enq0breq  7809  preqlu  7845  cnegexlem1  8508  neg11  8584  subeqrev  8709  cnref1o  10067  xneg11  10252  modlteq  10854  sq11  11069  qsqeqor  11107  fz1eqb  11250  eqwrd  11366  s111  11420  ccatopth  11509  wrd2ind  11516  cj11  11692  sqrt11  11826  sqabs  11870  recan  11897  reeff1  12491  efieq  12526  xpsff1o  13728  ismhm  13826  isdomn  14686  tgtop11  15319  ioocosf1o  16099  mpodvdsmulf1o  16301  iswlk  16786