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  5777  eqfnfv2  5778  f1mpt  5946  xpopth  6372  f1o2ndf1  6426  ecopoveq  6866  xpdom2  7084  djune  7371  addpipqqs  7687  enq0enq  7748  enq0sym  7749  enq0tr  7751  enq0breq  7753  preqlu  7789  cnegexlem1  8450  neg11  8526  subeqrev  8651  cnref1o  9986  xneg11  10170  modlteq  10763  sq11  10978  qsqeqor  11016  fz1eqb  11157  eqwrd  11269  s111  11323  ccatopth  11412  wrd2ind  11419  cj11  11594  sqrt11  11728  sqabs  11771  recan  11798  reeff1  12390  efieq  12425  xpsff1o  13579  ismhm  13691  isdomn  14432  tgtop11  14958  ioocosf1o  15736  mpodvdsmulf1o  15875  iswlk  16335