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 ⊢ ((𝜑 ∧ 𝜓) → (𝐴 = 𝐶 ↔ 𝐵 = 𝐷))

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105   = wceq 1402

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 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

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

This theorem is referenced by:  eqeqan12rd  2255  eqfnfv  5800  eqfnfv2  5801  f1mpt  5971  xpopth  6404  f1o2ndf1  6458  ecopoveq  6898  xpdom2  7123  djune  7412  addpipqqs  7731  enq0enq  7792  enq0sym  7793  enq0tr  7795  enq0breq  7797  preqlu  7833  cnegexlem1  8495  neg11  8571  subeqrev  8696  cnref1o  10034  xneg11  10219  modlteq  10817  sq11  11032  qsqeqor  11070  fz1eqb  11212  eqwrd  11328  s111  11382  ccatopth  11471  wrd2ind  11478  cj11  11654  sqrt11  11788  sqabs  11831  recan  11858  reeff1  12450  efieq  12485  xpsff1o  13653  ismhm  13751  isdomn  14561  tgtop11  15160  ioocosf1o  15938  mpodvdsmulf1o  16087  iswlk  16547