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

Theorem 3eqtrrd 2125
Description: A deduction from three chained equalities. (Contributed by NM, 4-Aug-2006.) (Proof shortened by Andrew Salmon, 25-May-2011.)
Hypotheses
Ref Expression
3eqtrd.1  |-  ( ph  ->  A  =  B )
3eqtrd.2  |-  ( ph  ->  B  =  C )
3eqtrd.3  |-  ( ph  ->  C  =  D )
Assertion
Ref Expression
3eqtrrd  |-  ( ph  ->  D  =  A )

Proof of Theorem 3eqtrrd
StepHypRef Expression
1 3eqtrd.1 . . 3  |-  ( ph  ->  A  =  B )
2 3eqtrd.2 . . 3  |-  ( ph  ->  B  =  C )
31, 2eqtrd 2120 . 2  |-  ( ph  ->  A  =  C )
4 3eqtrd.3 . 2  |-  ( ph  ->  C  =  D )
53, 4eqtr2d 2121 1  |-  ( ph  ->  D  =  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1289
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 1381  ax-gen 1383  ax-4 1445  ax-17 1464  ax-ext 2070
This theorem depends on definitions:  df-bi 115  df-cleq 2081
This theorem is referenced by:  nnanq0  7007  1idprl  7139  1idpru  7140  axcnre  7406  fseq1p1m1  9496  expmulzap  9989  expubnd  10000  subsq  10049  bcm1k  10156  bcpasc  10162  crim  10280  rereb  10285  fsumparts  10851  isumshft  10871  geosergap  10887  efsub  10958  sincossq  11026  efieq1re  11048  bezoutlema  11253  bezoutlemb  11254  eucialg  11306  phiprmpw  11463
  Copyright terms: Public domain W3C validator