Theorem eqeqan12d 2205

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 2202	. 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 2171

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

This theorem is referenced by:  eqeqan12rd  2206  eqfnfv  5634  eqfnfv2  5635  f1mpt  5793  xpopth  6202  f1o2ndf1  6254  ecopoveq  6657  xpdom2  6858  djune  7108  addpipqqs  7400  enq0enq  7461  enq0sym  7462  enq0tr  7464  enq0breq  7466  preqlu  7502  cnegexlem1  8163  neg11  8239  subeqrev  8364  cnref1o  9682  xneg11  9866  modlteq  10430  sq11  10627  qsqeqor  10665  fz1eqb  10805  cj11  10949  sqrt11  11083  sqabs  11126  recan  11153  reeff1  11743  efieq  11778  xpsff1o  12828  ismhm  12928  tgtop11  14053  ioocosf1o  14752