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

Theorem 3eqtrrd 2175
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 2170 . 2  |-  ( ph  ->  A  =  C )
4 3eqtrd.3 . 2  |-  ( ph  ->  C  =  D )
53, 4eqtr2d 2171 1  |-  ( ph  ->  D  =  A )
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 2119
This theorem depends on definitions:  df-bi 116  df-cleq 2130
This theorem is referenced by:  nnanq0  7259  1idprl  7391  1idpru  7392  axcnre  7682  fseq1p1m1  9867  expmulzap  10332  expubnd  10343  subsq  10392  bcm1k  10499  bcpasc  10505  crim  10623  rereb  10628  fsumparts  11232  isumshft  11252  geosergap  11268  efsub  11376  sincossq  11444  efieq1re  11467  bezoutlema  11676  bezoutlemb  11677  eucalg  11729  phiprmpw  11887  strsetsid  11981  setsslid  11998  upxp  12430  uptx  12432
  Copyright terms: Public domain W3C validator