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  5806  eqfnfv2  5807  f1mpt  5977  xpopth  6410  f1o2ndf1  6464  ecopoveq  6904  xpdom2  7129  djune  7418  addpipqqs  7737  enq0enq  7798  enq0sym  7799  enq0tr  7801  enq0breq  7803  preqlu  7839  cnegexlem1  8501  neg11  8577  subeqrev  8702  cnref1o  10053  xneg11  10238  modlteq  10836  sq11  11051  qsqeqor  11089  fz1eqb  11231  eqwrd  11347  s111  11401  ccatopth  11490  wrd2ind  11497  cj11  11673  sqrt11  11807  sqabs  11850  recan  11877  reeff1  12469  efieq  12504  xpsff1o  13672  ismhm  13770  isdomn  14580  tgtop11  15179  ioocosf1o  15958  mpodvdsmulf1o  16110  iswlk  16576