Theorem eqeqan12d 2155

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

Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104   = wceq 1331

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-gen 1425  ax-4 1487  ax-17 1506  ax-ext 2121

This theorem depends on definitions:  df-bi 116  df-cleq 2132

This theorem is referenced by:  eqeqan12rd  2156  eqfnfv  5518  eqfnfv2  5519  f1mpt  5672  xpopth  6074  f1o2ndf1  6125  ecopoveq  6524  xpdom2  6725  djune  6963  addpipqqs  7178  enq0enq  7239  enq0sym  7240  enq0tr  7242  enq0breq  7244  preqlu  7280  cnegexlem1  7937  neg11  8013  subeqrev  8138  cnref1o  9440  xneg11  9617  modlteq  10170  sq11  10365  fz1eqb  10537  cj11  10677  sqrt11  10811  sqabs  10854  recan  10881  reeff1  11407  efieq  11442  tgtop11  12245