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  3114  disjdif2  3503  dfopg  3778  xpid11  4852  sqxpeq0  5054  cores2  5143  funcoeqres  5494  dftpos2  6265  ine0  8354  fisumcom2  11449  fisum0diag2  11458  mertenslemi1  11546  fprodcom2fi  11637  fprodmodd  11652  4sqlem10  12388  setsslnid  12517  xpsff1o  12774  eqglact  13090  oppr1g  13258  dvmptccn  14319  nninffeq  14909
  Copyright terms: Public domain W3C validator