Theorem eqeqan12d 2250

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 2247	. 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 = 𝐶 ↔ 𝐵 = 𝐷))
4	1, 2, 3	syl2an 289	1 ⊢ ((𝜑 ∧ 𝜓) → (𝐴 = 𝐶 ↔ 𝐵 = 𝐷))

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 2216

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

This theorem is referenced by:  eqeqan12rd  2251  eqfnfv  5780  eqfnfv2  5781  f1mpt  5950  xpopth  6383  f1o2ndf1  6437  ecopoveq  6877  xpdom2  7095  djune  7382  addpipqqs  7701  enq0enq  7762  enq0sym  7763  enq0tr  7765  enq0breq  7767  preqlu  7803  cnegexlem1  8465  neg11  8541  subeqrev  8666  cnref1o  10004  xneg11  10189  modlteq  10786  sq11  11001  qsqeqor  11039  fz1eqb  11181  eqwrd  11293  s111  11347  ccatopth  11436  wrd2ind  11443  cj11  11619  sqrt11  11753  sqabs  11796  recan  11823  reeff1  12415  efieq  12450  xpsff1o  13617  ismhm  13720  isdomn  14520  tgtop11  15071  ioocosf1o  15849  mpodvdsmulf1o  15988  iswlk  16448