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

Theorem 3eqtrrd 2155
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 2150 . 2  |-  ( ph  ->  A  =  C )
4 3eqtrd.3 . 2  |-  ( ph  ->  C  =  D )
53, 4eqtr2d 2151 1  |-  ( ph  ->  D  =  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1316
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 1408  ax-gen 1410  ax-4 1472  ax-17 1491  ax-ext 2099
This theorem depends on definitions:  df-bi 116  df-cleq 2110
This theorem is referenced by:  nnanq0  7234  1idprl  7366  1idpru  7367  axcnre  7657  fseq1p1m1  9842  expmulzap  10307  expubnd  10318  subsq  10367  bcm1k  10474  bcpasc  10480  crim  10598  rereb  10603  fsumparts  11207  isumshft  11227  geosergap  11243  efsub  11314  sincossq  11382  efieq1re  11405  bezoutlema  11614  bezoutlemb  11615  eucalg  11667  phiprmpw  11825  strsetsid  11919  setsslid  11936  upxp  12368  uptx  12370
  Copyright terms: Public domain W3C validator