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	⊢ (𝜑 → 𝐴 = 𝐵)
eqeqan12d.2	⊢ (𝜓 → 𝐶 = 𝐷)

Assertion

Ref	Expression
eqeqan12d	⊢ ((𝜑 ∧ 𝜓) → (𝐴 = 𝐶 ↔ 𝐵 = 𝐷))

Proof of Theorem eqeqan12d

Step	Hyp	Ref	Expression
1		eqeqan12d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		eqeqan12d.2	. 2 ⊢ (𝜓 → 𝐶 = 𝐷)
3		eqeq12 2251	. 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 = 𝐶 ↔ 𝐵 = 𝐷))
4	1, 2, 3	syl2an 289	1 ⊢ ((𝜑 ∧ 𝜓) → (𝐴 = 𝐶 ↔ 𝐵 = 𝐷))

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  6908  xpdom2  7134  djune  7425  addpipqqs  7744  enq0enq  7805  enq0sym  7806  enq0tr  7808  enq0breq  7810  preqlu  7846  cnegexlem1  8509  neg11  8585  subeqrev  8710  cnref1o  10069  xneg11  10254  modlteq  10856  sq11  11071  qsqeqor  11109  fz1eqb  11252  eqwrd  11368  s111  11422  ccatopth  11511  wrd2ind  11518  cj11  11694  sqrt11  11828  sqabs  11872  recan  11899  reeff1  12493  efieq  12528  xpsff1o  13730  ismhm  13828  isdomn  14688  tgtop11  15314  ioocosf1o  16094  mpodvdsmulf1o  16296  iswlk  16781