Theorem eqeqan12d 2245

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

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

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 1493  ax-gen 1495  ax-4 1556  ax-17 1572  ax-ext 2211

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

This theorem is referenced by:  eqeqan12rd  2246  eqfnfv  5734  eqfnfv2  5735  f1mpt  5901  xpopth  6328  f1o2ndf1  6380  ecopoveq  6785  xpdom2  6998  djune  7253  addpipqqs  7565  enq0enq  7626  enq0sym  7627  enq0tr  7629  enq0breq  7631  preqlu  7667  cnegexlem1  8329  neg11  8405  subeqrev  8530  cnref1o  9854  xneg11  10038  modlteq  10627  sq11  10842  qsqeqor  10880  fz1eqb  11020  eqwrd  11120  s111  11172  ccatopth  11256  wrd2ind  11263  cj11  11424  sqrt11  11558  sqabs  11601  recan  11628  reeff1  12219  efieq  12254  xpsff1o  13390  ismhm  13502  isdomn  14241  tgtop11  14758  ioocosf1o  15536  mpodvdsmulf1o  15672  iswlk  16044