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

Theorem 3eqtr4rd 2183
Description: A deduction from three chained equalities. (Contributed by NM, 21-Sep-1995.)
Hypotheses
Ref Expression
3eqtr4d.1  |-  ( ph  ->  A  =  B )
3eqtr4d.2  |-  ( ph  ->  C  =  A )
3eqtr4d.3  |-  ( ph  ->  D  =  B )
Assertion
Ref Expression
3eqtr4rd  |-  ( ph  ->  D  =  C )

Proof of Theorem 3eqtr4rd
StepHypRef Expression
1 3eqtr4d.3 . . 3  |-  ( ph  ->  D  =  B )
2 3eqtr4d.1 . . 3  |-  ( ph  ->  A  =  B )
31, 2eqtr4d 2175 . 2  |-  ( ph  ->  D  =  A )
4 3eqtr4d.2 . 2  |-  ( ph  ->  C  =  A )
53, 4eqtr4d 2175 1  |-  ( ph  ->  D  =  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1331
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 1423  ax-gen 1425  ax-4 1487  ax-17 1506  ax-ext 2121
This theorem depends on definitions:  df-bi 116  df-cleq 2132
This theorem is referenced by:  csbcnvg  4723  fvco4  5493  phplem4  6749  phplem4on  6761  omp1eomlem  6979  ctssdclemn0  6995  recexnq  7210  prarloclemcalc  7322  addcomprg  7398  mulcomprg  7400  mulcmpblnrlemg  7560  axmulass  7693  divnegap  8478  modqlt  10118  modqmulnn  10127  seq3val  10243  seqvalcd  10244  seq3caopr3  10266  seq3f1olemqsumkj  10283  seq3f1olemqsumk  10284  seq3f1olemqsum  10285  seq3f1o  10289  bcval5  10521  omgadd  10560  seq3coll  10597  cjreb  10650  recj  10651  imcj  10659  imval2  10678  resqrexlemover  10794  sqrtmul  10819  amgm2  10902  maxabslemab  10990  xrmaxadd  11042  summodclem2a  11162  fsumf1o  11171  sumsnf  11190  sumsplitdc  11213  fsummulc2  11229  binom  11265  bcxmas  11270  expcnvap0  11283  expcnv  11285  cvgratnnlemnexp  11305  cvgratnnlemmn  11306  prodmodclem3  11356  ege2le3  11389  efaddlem  11392  eftlub  11408  tanval3ap  11432  tannegap  11446  cosmul  11463  cos01bnd  11476  demoivreALT  11491  flodddiv4  11642  dfgcd3  11709  absmulgcd  11716  sqpweven  11864  2sqpwodd  11865  crth  11911  ctiunctlemfo  11963  setsslnid  12024  txbasval  12450
  Copyright terms: Public domain W3C validator