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 1397

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 1495  ax-gen 1497  ax-4 1558  ax-17 1574  ax-ext 2213

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

This theorem is referenced by:  eqeqan12rd  2248  eqfnfv  5744  eqfnfv2  5745  f1mpt  5912  xpopth  6339  f1o2ndf1  6393  ecopoveq  6799  xpdom2  7015  djune  7277  addpipqqs  7590  enq0enq  7651  enq0sym  7652  enq0tr  7654  enq0breq  7656  preqlu  7692  cnegexlem1  8354  neg11  8430  subeqrev  8555  cnref1o  9885  xneg11  10069  modlteq  10660  sq11  10875  qsqeqor  10913  fz1eqb  11053  eqwrd  11158  s111  11212  ccatopth  11301  wrd2ind  11308  cj11  11470  sqrt11  11604  sqabs  11647  recan  11674  reeff1  12266  efieq  12301  xpsff1o  13437  ismhm  13549  isdomn  14289  tgtop11  14806  ioocosf1o  15584  mpodvdsmulf1o  15720  iswlk  16180