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

Assertion

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

Proof of Theorem eqeqan12d

Step	Hyp	Ref	Expression
1		eqeqan12d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		eqeqan12d.2	. 2 ⊢ (𝜓 → 𝐶 = 𝐷)
3		eqeq12 2245	. 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 2214

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

This theorem is referenced by:  eqeqan12rd  2249  eqfnfv  5774  eqfnfv2  5775  f1mpt  5943  xpopth  6369  f1o2ndf1  6423  ecopoveq  6863  xpdom2  7081  djune  7368  addpipqqs  7684  enq0enq  7745  enq0sym  7746  enq0tr  7748  enq0breq  7750  preqlu  7786  cnegexlem1  8447  neg11  8523  subeqrev  8648  cnref1o  9982  xneg11  10166  modlteq  10758  sq11  10973  qsqeqor  11011  fz1eqb  11151  eqwrd  11261  s111  11315  ccatopth  11404  wrd2ind  11411  cj11  11586  sqrt11  11720  sqabs  11763  recan  11790  reeff1  12382  efieq  12417  xpsff1o  13554  ismhm  13666  isdomn  14407  tgtop11  14933  ioocosf1o  15711  mpodvdsmulf1o  15850  iswlk  16310