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

Theorem 3eqtr3g 2171
 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, 2syl5eqr 2162 . 2 (𝜑𝐶 = 𝐵)
4 3eqtr3g.3 . 2 𝐵 = 𝐷
53, 4syl6eq 2164 1 (𝜑𝐶 = 𝐷)
 Colors of variables: wff set class Syntax hints:   → wi 4   = wceq 1314 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 1406  ax-gen 1408  ax-4 1470  ax-17 1489  ax-ext 2097 This theorem depends on definitions:  df-bi 116  df-cleq 2108 This theorem is referenced by:  csbnest1g  3023  disjdif2  3409  dfopg  3671  xpid11  4730  sqxpeq0  4930  cores2  5019  funcoeqres  5364  dftpos2  6124  ine0  8120  fisumcom2  11158  fisum0diag2  11167  mertenslemi1  11255  setsslnid  11916  dvmptccn  12754  nninffeq  13050
 Copyright terms: Public domain W3C validator