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

Theorem 3eqtr3g 2233
Description: A chained equality inference, useful for converting from definitions. (Contributed by NM, 15-Nov-1994.)
Hypotheses
Ref Expression
3eqtr3g.1 (𝜑𝐴 = 𝐵)
3eqtr3g.2 𝐴 = 𝐶
3eqtr3g.3 𝐵 = 𝐷
Assertion
Ref Expression
3eqtr3g (𝜑𝐶 = 𝐷)

Proof of Theorem 3eqtr3g
StepHypRef Expression
1 3eqtr3g.2 . . 3 𝐴 = 𝐶
2 3eqtr3g.1 . . 3 (𝜑𝐴 = 𝐵)
31, 2eqtr3id 2224 . 2 (𝜑𝐶 = 𝐵)
4 3eqtr3g.3 . 2 𝐵 = 𝐷
53, 4eqtrdi 2226 1 (𝜑𝐶 = 𝐷)
Colors of variables: wff set class
Syntax hints:  wi 4   = 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:  csbnest1g  3112  disjdif2  3501  dfopg  3776  xpid11  4850  sqxpeq0  5052  cores2  5141  funcoeqres  5492  dftpos2  6261  ine0  8349  fisumcom2  11441  fisum0diag2  11450  mertenslemi1  11538  fprodcom2fi  11629  fprodmodd  11644  4sqlem10  12379  setsslnid  12508  eqglact  13037  oppr1g  13205  dvmptccn  14072  nninffeq  14651
  Copyright terms: Public domain W3C validator