Theorem eqeqan12d 2209

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 2206	. 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 1458  ax-gen 1460  ax-4 1521  ax-17 1537  ax-ext 2175

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

This theorem is referenced by:  eqeqan12rd  2210  eqfnfv  5656  eqfnfv2  5657  f1mpt  5815  xpopth  6231  f1o2ndf1  6283  ecopoveq  6686  xpdom2  6887  djune  7139  addpipqqs  7432  enq0enq  7493  enq0sym  7494  enq0tr  7496  enq0breq  7498  preqlu  7534  cnegexlem1  8196  neg11  8272  subeqrev  8397  cnref1o  9719  xneg11  9903  modlteq  10471  sq11  10686  qsqeqor  10724  fz1eqb  10864  eqwrd  10957  cj11  11052  sqrt11  11186  sqabs  11229  recan  11256  reeff1  11846  efieq  11881  xpsff1o  12935  ismhm  13036  isdomn  13768  tgtop11  14255  ioocosf1o  15030