Theorem eqeqan12d 2222

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

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

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 1471  ax-gen 1473  ax-4 1534  ax-17 1550  ax-ext 2188

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

This theorem is referenced by:  eqeqan12rd  2223  eqfnfv  5687  eqfnfv2  5688  f1mpt  5850  xpopth  6272  f1o2ndf1  6324  ecopoveq  6727  xpdom2  6938  djune  7192  addpipqqs  7496  enq0enq  7557  enq0sym  7558  enq0tr  7560  enq0breq  7562  preqlu  7598  cnegexlem1  8260  neg11  8336  subeqrev  8461  cnref1o  9785  xneg11  9969  modlteq  10555  sq11  10770  qsqeqor  10808  fz1eqb  10948  eqwrd  11047  s111  11099  cj11  11266  sqrt11  11400  sqabs  11443  recan  11470  reeff1  12061  efieq  12096  xpsff1o  13231  ismhm  13343  isdomn  14081  tgtop11  14598  ioocosf1o  15376  mpodvdsmulf1o  15512