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

Theorem eqeqan12d 2193
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 2190 . 2 ((𝐴 = 𝐵𝐶 = 𝐷) → (𝐴 = 𝐶𝐵 = 𝐷))
41, 2, 3syl2an 289 1 ((𝜑𝜓) → (𝐴 = 𝐶𝐵 = 𝐷))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104  wb 105   = wceq 1353
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 1447  ax-gen 1449  ax-4 1510  ax-17 1526  ax-ext 2159
This theorem depends on definitions:  df-bi 117  df-cleq 2170
This theorem is referenced by:  eqeqan12rd  2194  eqfnfv  5608  eqfnfv2  5609  f1mpt  5765  xpopth  6170  f1o2ndf1  6222  ecopoveq  6623  xpdom2  6824  djune  7070  addpipqqs  7347  enq0enq  7408  enq0sym  7409  enq0tr  7411  enq0breq  7413  preqlu  7449  cnegexlem1  8109  neg11  8185  subeqrev  8310  cnref1o  9626  xneg11  9808  modlteq  10370  sq11  10565  qsqeqor  10603  fz1eqb  10741  cj11  10885  sqrt11  11019  sqabs  11062  recan  11089  reeff1  11679  efieq  11714  ismhm  12730  tgtop11  13209  ioocosf1o  13908
  Copyright terms: Public domain W3C validator