ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  eqeqan12d GIF version

Theorem eqeqan12d 2205
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
StepHypRef Expression
1 eqeqan12d.1 . 2 (𝜑𝐴 = 𝐵)
2 eqeqan12d.2 . 2 (𝜓𝐶 = 𝐷)
3 eqeq12 2202 . 2 ((𝐴 = 𝐵𝐶 = 𝐷) → (𝐴 = 𝐶𝐵 = 𝐷))
41, 2, 3syl2an 289 1 ((𝜑𝜓) → (𝐴 = 𝐶𝐵 = 𝐷))
Colors of variables: wff set class
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 1458  ax-gen 1460  ax-4 1521  ax-17 1537  ax-ext 2171
This theorem depends on definitions:  df-bi 117  df-cleq 2182
This theorem is referenced by:  eqeqan12rd  2206  eqfnfv  5634  eqfnfv2  5635  f1mpt  5793  xpopth  6202  f1o2ndf1  6254  ecopoveq  6657  xpdom2  6858  djune  7108  addpipqqs  7400  enq0enq  7461  enq0sym  7462  enq0tr  7464  enq0breq  7466  preqlu  7502  cnegexlem1  8163  neg11  8239  subeqrev  8364  cnref1o  9682  xneg11  9866  modlteq  10430  sq11  10627  qsqeqor  10665  fz1eqb  10805  cj11  10949  sqrt11  11083  sqabs  11126  recan  11153  reeff1  11743  efieq  11778  xpsff1o  12828  ismhm  12928  tgtop11  14053  ioocosf1o  14752
  Copyright terms: Public domain W3C validator