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

Theorem 3eqtr3rd 2219
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 2212 . 2  |-  ( ph  ->  B  =  C )
51, 4eqtr3d 2212 1  |-  ( ph  ->  D  =  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1353
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1447  ax-gen 1449  ax-4 1510  ax-17 1526  ax-ext 2159
This theorem depends on definitions:  df-bi 117  df-cleq 2170
This theorem is referenced by:  fcofo  5785  fcof1o  5790  frecabcl  6400  nnaword  6512  nninfisol  7131  enomnilem  7136  fodju0  7145  enmkvlem  7159  enwomnilem  7167  pn0sr  7770  negeu  8148  add20  8431  2halves  9148  bcnn  10737  bcpasc  10746  resqrexlemover  11019  fsumneg  11459  geolim  11519  geolim2  11520  mertensabs  11545  sincossq  11756  demoivre  11780  eirraplem  11784  gcdid  11987  gcdmultipled  11994  phiprmpw  12222  pythagtriplem12  12275  expnprm  12351  imasbas  12728  imasplusg  12729  imasmulr  12730  grpinvid1  12924  grpnpcan  12962  grplactcnv  12972  ghmgrp  12982  ringnegl  13228  ringnegr  13229  ringmneg2  13231  ring1  13236  rdivmuldivd  13313  lmodfopne  13416  lmodvsneg  13421  ioo2bl  14046  ptolemy  14248  coskpi  14272  logbgcd1irr  14388  logbgcd1irraplemap  14390
  Copyright terms: Public domain W3C validator