Theorem eqeqan12d 2186

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

Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104   = wceq 1348

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-gen 1442  ax-4 1503  ax-17 1519  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-cleq 2163

This theorem is referenced by:  eqeqan12rd  2187  eqfnfv  5593  eqfnfv2  5594  f1mpt  5750  xpopth  6155  f1o2ndf1  6207  ecopoveq  6608  xpdom2  6809  djune  7055  addpipqqs  7332  enq0enq  7393  enq0sym  7394  enq0tr  7396  enq0breq  7398  preqlu  7434  cnegexlem1  8094  neg11  8170  subeqrev  8295  cnref1o  9609  xneg11  9791  modlteq  10353  sq11  10548  qsqeqor  10586  fz1eqb  10725  cj11  10869  sqrt11  11003  sqabs  11046  recan  11073  reeff1  11663  efieq  11698  ismhm  12685  tgtop11  12870  ioocosf1o  13569