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

Theorem eqeqan12d 2156
 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 2153 . 2 ((𝐴 = 𝐵𝐶 = 𝐷) → (𝐴 = 𝐶𝐵 = 𝐷))
41, 2, 3syl2an 287 1 ((𝜑𝜓) → (𝐴 = 𝐶𝐵 = 𝐷))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104   = wceq 1332 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 1424  ax-gen 1426  ax-4 1488  ax-17 1507  ax-ext 2122 This theorem depends on definitions:  df-bi 116  df-cleq 2133 This theorem is referenced by:  eqeqan12rd  2157  eqfnfv  5529  eqfnfv2  5530  f1mpt  5683  xpopth  6085  f1o2ndf1  6136  ecopoveq  6535  xpdom2  6736  djune  6979  addpipqqs  7229  enq0enq  7290  enq0sym  7291  enq0tr  7293  enq0breq  7295  preqlu  7331  cnegexlem1  7988  neg11  8064  subeqrev  8189  cnref1o  9496  xneg11  9674  modlteq  10228  sq11  10423  fz1eqb  10596  cj11  10736  sqrt11  10870  sqabs  10913  recan  10940  reeff1  11477  efieq  11512  tgtop11  12318  ioocosf1o  13017
 Copyright terms: Public domain W3C validator