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

Theorem 3eqtr4a 2140
Description: A chained equality inference, useful for converting to definitions. (Contributed by NM, 2-Feb-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.)
Hypotheses
Ref Expression
3eqtr4a.1  |-  A  =  B
3eqtr4a.2  |-  ( ph  ->  C  =  A )
3eqtr4a.3  |-  ( ph  ->  D  =  B )
Assertion
Ref Expression
3eqtr4a  |-  ( ph  ->  C  =  D )

Proof of Theorem 3eqtr4a
StepHypRef Expression
1 3eqtr4a.2 . . 3  |-  ( ph  ->  C  =  A )
2 3eqtr4a.1 . . 3  |-  A  =  B
31, 2syl6eq 2130 . 2  |-  ( ph  ->  C  =  B )
4 3eqtr4a.3 . 2  |-  ( ph  ->  D  =  B )
53, 4eqtr4d 2117 1  |-  ( ph  ->  C  =  D )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1285
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1377  ax-gen 1379  ax-4 1441  ax-17 1460  ax-ext 2064
This theorem depends on definitions:  df-bi 115  df-cleq 2075
This theorem is referenced by:  uniintsnr  3680  fndmdifcom  5305  offres  5793  1stval2  5813  2ndval2  5814  ecovcom  6279  ecovass  6281  ecovdi  6283  zeo  8533  xnegneg  8976  fzsuc2  9172  expnegap0  9581  facp1  9754  bcpasc  9790  absexp  10103  gcdcom  10509  gcd0id  10514  dfgcd3  10543  gcdass  10548  lcmcom  10590  lcmneg  10600  lcmass  10611  sqrt2irrlem  10684
  Copyright terms: Public domain W3C validator