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

Theorem eqeqan12d 2055
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 2052 . 2 ((𝐴 = 𝐵𝐶 = 𝐷) → (𝐴 = 𝐶𝐵 = 𝐷))
41, 2, 3syl2an 273 1 ((𝜑𝜓) → (𝐴 = 𝐶𝐵 = 𝐷))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 97  wb 98   = wceq 1243
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-gen 1338  ax-4 1400  ax-17 1419  ax-ext 2022
This theorem depends on definitions:  df-bi 110  df-cleq 2033
This theorem is referenced by:  eqeqan12rd  2056  eqfnfv  5265  eqfnfv2  5266  f1mpt  5410  xpopth  5802  f1o2ndf1  5849  ecopoveq  6201  xpdom2  6305  addpipqqs  6468  enq0enq  6529  enq0sym  6530  enq0tr  6532  enq0breq  6534  preqlu  6570  cnegexlem1  7186  neg11  7262  subeqrev  7374  cnref1o  8582  xneg11  8747  sq11  9326  cj11  9505  sqrt11  9637  sqabs  9678  recan  9705
  Copyright terms: Public domain W3C validator