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  8464  neg11  8540  subeqrev  8665  cnref1o  10001  xneg11  10186  modlteq  10783  sq11  10998  qsqeqor  11036  fz1eqb  11178  eqwrd  11290  s111  11344  ccatopth  11433  wrd2ind  11440  cj11  11615  sqrt11  11749  sqabs  11792  recan  11819  reeff1  12411  efieq  12446  xpsff1o  13646  ismhm  13758  isdomn  14501  tgtop11  15053  ioocosf1o  15831  mpodvdsmulf1o  15970  iswlk  16430