Theorem eqeqan12d 2212

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 2209	. 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 1461  ax-gen 1463  ax-4 1524  ax-17 1540  ax-ext 2178

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

This theorem is referenced by:  eqeqan12rd  2213  eqfnfv  5659  eqfnfv2  5660  f1mpt  5818  xpopth  6234  f1o2ndf1  6286  ecopoveq  6689  xpdom2  6890  djune  7144  addpipqqs  7437  enq0enq  7498  enq0sym  7499  enq0tr  7501  enq0breq  7503  preqlu  7539  cnegexlem1  8201  neg11  8277  subeqrev  8402  cnref1o  9725  xneg11  9909  modlteq  10489  sq11  10704  qsqeqor  10742  fz1eqb  10882  eqwrd  10975  cj11  11070  sqrt11  11204  sqabs  11247  recan  11274  reeff1  11865  efieq  11900  xpsff1o  12992  ismhm  13093  isdomn  13825  tgtop11  14312  ioocosf1o  15090  mpodvdsmulf1o  15226