Theorem eqeqan12d 2212

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 2209	. 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 = 𝐶 ↔ 𝐵 = 𝐷))
4	1, 2, 3	syl2an 289	1 ⊢ ((𝜑 ∧ 𝜓) → (𝐴 = 𝐶 ↔ 𝐵 = 𝐷))

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

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 1461  ax-gen 1463  ax-4 1524  ax-17 1540  ax-ext 2178

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

This theorem is referenced by:  eqeqan12rd  2213  eqfnfv  5662  eqfnfv2  5663  f1mpt  5821  xpopth  6243  f1o2ndf1  6295  ecopoveq  6698  xpdom2  6899  djune  7153  addpipqqs  7454  enq0enq  7515  enq0sym  7516  enq0tr  7518  enq0breq  7520  preqlu  7556  cnegexlem1  8218  neg11  8294  subeqrev  8419  cnref1o  9742  xneg11  9926  modlteq  10506  sq11  10721  qsqeqor  10759  fz1eqb  10899  eqwrd  10992  cj11  11087  sqrt11  11221  sqabs  11264  recan  11291  reeff1  11882  efieq  11917  xpsff1o  13051  ismhm  13163  isdomn  13901  tgtop11  14396  ioocosf1o  15174  mpodvdsmulf1o  15310