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

Theorem 3eqtr3rd 2129
Description: A deduction from three chained equalities. (Contributed by NM, 14-Jan-2006.)
Hypotheses
Ref Expression
3eqtr3d.1  |-  ( ph  ->  A  =  B )
3eqtr3d.2  |-  ( ph  ->  A  =  C )
3eqtr3d.3  |-  ( ph  ->  B  =  D )
Assertion
Ref Expression
3eqtr3rd  |-  ( ph  ->  D  =  C )

Proof of Theorem 3eqtr3rd
StepHypRef Expression
1 3eqtr3d.3 . 2  |-  ( ph  ->  B  =  D )
2 3eqtr3d.1 . . 3  |-  ( ph  ->  A  =  B )
3 3eqtr3d.2 . . 3  |-  ( ph  ->  A  =  C )
42, 3eqtr3d 2122 . 2  |-  ( ph  ->  B  =  C )
51, 4eqtr3d 2122 1  |-  ( ph  ->  D  =  C )
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:  fcofo  5563  fcof1o  5568  frecabcl  6164  nnaword  6268  enomnilem  6792  fodjuomnilem0  6800  pn0sr  7315  negeu  7671  add20  7950  2halves  8643  bcnn  10161  bcpasc  10170  resqrexlemover  10439  fsumneg  10841  geolim  10901  geolim2  10902  mertensabs  10927  sincossq  11035  demoivre  11058  eirraplem  11060  gcdid  11251  phiprmpw  11472
  Copyright terms: Public domain W3C validator