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

Theorem eqeqan12d 2052
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 (φA = B)
eqeqan12d.2 (ψ𝐶 = 𝐷)
Assertion
Ref Expression
eqeqan12d ((φ ψ) → (A = 𝐶B = 𝐷))

Proof of Theorem eqeqan12d
StepHypRef Expression
1 eqeqan12d.1 . 2 (φA = B)
2 eqeqan12d.2 . 2 (ψ𝐶 = 𝐷)
3 eqeq12 2049 . 2 ((A = B 𝐶 = 𝐷) → (A = 𝐶B = 𝐷))
41, 2, 3syl2an 273 1 ((φ ψ) → (A = 𝐶B = 𝐷))
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97  wb 98   = wceq 1242
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 1333  ax-gen 1335  ax-4 1397  ax-17 1416  ax-ext 2019
This theorem depends on definitions:  df-bi 110  df-cleq 2030
This theorem is referenced by:  eqeqan12rd  2053  eqfnfv  5208  eqfnfv2  5209  f1mpt  5353  xpopth  5744  f1o2ndf1  5791  ecopoveq  6137  xpdom2  6241  addpipqqs  6354  enq0enq  6414  enq0sym  6415  enq0tr  6417  enq0breq  6419  preqlu  6455  cnegexlem1  6983  neg11  7058  subeqrev  7170  cnref1o  8357  xneg11  8517  sq11  8979  cj11  9133
  Copyright terms: Public domain W3C validator