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

Theorem eqeqan12d 2115
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 2112 . 2 ((𝐴 = 𝐵𝐶 = 𝐷) → (𝐴 = 𝐶𝐵 = 𝐷))
41, 2, 3syl2an 285 1 ((𝜑𝜓) → (𝐴 = 𝐶𝐵 = 𝐷))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  wb 104   = wceq 1299
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1391  ax-gen 1393  ax-4 1455  ax-17 1474  ax-ext 2082
This theorem depends on definitions:  df-bi 116  df-cleq 2093
This theorem is referenced by:  eqeqan12rd  2116  eqfnfv  5450  eqfnfv2  5451  f1mpt  5604  xpopth  6004  f1o2ndf1  6055  ecopoveq  6454  xpdom2  6654  djune  6878  addpipqqs  7079  enq0enq  7140  enq0sym  7141  enq0tr  7143  enq0breq  7145  preqlu  7181  cnegexlem1  7808  neg11  7884  subeqrev  8005  cnref1o  9290  xneg11  9458  modlteq  10011  sq11  10206  fz1eqb  10378  cj11  10518  sqrt11  10651  sqabs  10694  recan  10721  reeff1  11205  efieq  11240  tgtop11  12027
  Copyright terms: Public domain W3C validator