Theorem eqeqan12d 2247

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 2244	. 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 2213

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

This theorem is referenced by:  eqeqan12rd  2248  eqfnfv  5753  eqfnfv2  5754  f1mpt  5922  xpopth  6348  f1o2ndf1  6402  ecopoveq  6842  xpdom2  7058  djune  7320  addpipqqs  7633  enq0enq  7694  enq0sym  7695  enq0tr  7697  enq0breq  7699  preqlu  7735  cnegexlem1  8397  neg11  8473  subeqrev  8598  cnref1o  9928  xneg11  10112  modlteq  10703  sq11  10918  qsqeqor  10956  fz1eqb  11096  eqwrd  11201  s111  11255  ccatopth  11344  wrd2ind  11351  cj11  11526  sqrt11  11660  sqabs  11703  recan  11730  reeff1  12322  efieq  12357  xpsff1o  13493  ismhm  13605  isdomn  14345  tgtop11  14867  ioocosf1o  15645  mpodvdsmulf1o  15784  iswlk  16244