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

Theorem 3eqtr4a 2248
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, 2eqtrdi 2238 . 2  |-  ( ph  ->  C  =  B )
4 3eqtr4a.3 . 2  |-  ( ph  ->  D  =  B )
53, 4eqtr4d 2225 1  |-  ( ph  ->  C  =  D )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1364
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 1458  ax-gen 1460  ax-4 1521  ax-17 1537  ax-ext 2171
This theorem depends on definitions:  df-bi 117  df-cleq 2182
This theorem is referenced by:  uniintsnr  3895  fndmdifcom  5638  offres  6154  1stval2  6174  2ndval2  6175  ecovcom  6660  ecovass  6662  ecovdi  6664  nnnninfeq2  7145  zeo  9376  xnegneg  9851  xaddcom  9879  xaddid1  9880  xnegdi  9886  fzsuc2  10097  expnegap0  10546  facp1  10728  bcpasc  10764  hashfzp1  10822  resunimafz0  10829  absexp  11106  iooinsup  11303  fsumf1o  11416  fsumadd  11432  fisumrev2  11472  fsumparts  11496  fprodf1o  11614  fprodmul  11617  efexp  11708  tanval2ap  11739  gcdcom  11992  gcd0id  11998  dfgcd3  12029  gcdass  12034  lcmcom  12082  lcmneg  12092  lcmass  12103  sqrt2irrlem  12179  nn0gcdsq  12218  dfphi2  12238  eulerthlemth  12250  pcneg  12342  setscom  12520  restco  14071  txtopon  14159  dvef  14585  lgsneg  14822  lgsneg1  14823  lgsdir2  14831  lgsdir  14833  lgsdi  14835
  Copyright terms: Public domain W3C validator