MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3eqtr3rd Structured version   Unicode version

Theorem 3eqtr3rd 2474
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 2467 . 2  |-  ( ph  ->  B  =  C )
51, 4eqtr3d 2467 1  |-  ( ph  ->  D  =  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1362
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-12 1791  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-ex 1590  df-cleq 2426
This theorem is referenced by:  fcofo  5979  fcof1o  5984  cantnfp1lem3  7876  cantnfp1lem3OLD  7902  fin1a2lem7  8563  prlem934  9190  addid2  9540  addcom  9543  addcomd  9559  negeu  9588  add20  9839  2halves  10541  bcnn  12072  bcpasc  12081  hashfun  12183  wrdeqs1cat  12353  sqreulem  12831  summolem3  13175  fsumneg  13237  geolim  13313  geolim2  13314  mertens  13329  sincossq  13443  demoivre  13467  eirrlem  13469  sadeq  13651  gcdid  13698  phiprmpw  13834  pythagtriplem12  13876  expnprm  13947  fullresc  14744  grpinvid1  15566  grpnpcan  15597  grplactcnv  15604  conjghm  15757  odmodnn0  16023  gex1  16070  sylow3lem3  16108  efgredeu  16229  odadd2  16311  gsumval3OLD  16362  gsumval3  16365  pgpfac1lem3a  16551  rngnegl  16620  rngnegr  16621  rngmneg2  16623  lmodvsneg  16913  lss0v  17019  lssvs0or  17113  lvecinv  17116  lspabs2  17123  mplcoe3  17479  mplcoe3OLD  17480  mplcoe2  17481  mplcoe2OLD  17482  zringcyg  17749  zcyg  17754  zringunit  17756  zrngunit  17757  mdetrlin  18251  mdetunilem6  18265  cramerimplem3  18333  cramerimp  18334  paste  18740  tuslem  19684  tususs  19687  ngpds  20037  ioo2bl  20212  ipcau2  20591  cmetcusp  20708  dvexp3  21292  rolle  21304  cmvth  21305  dv11cn  21315  lhop  21330  itgsubstlem  21362  ply1divex  21493  fta1glem1  21522  fta1g  21524  fta1  21659  vieta1lem2  21662  aaliou2  21691  dvtaylp  21720  dvntaylp  21721  taylthlem1  21723  taylthlem2  21724  dvradcnv  21771  ptolemy  21843  coskpi  21867  tanregt0  21880  cxpeq  22080  isosctrlem2  22102  chordthmlem  22112  dcubic  22126  quart1lem  22135  tanatan  22199  atantan  22203  dvatan  22215  birthdaylem2  22231  rlimcxp  22252  jensenlem2  22266  logdiflbnd  22273  emcllem2  22275  basellem8  22310  bclbnd  22504  lgsqr  22570  lgseisenlem3  22575  lgseisenlem4  22576  lgsquadlem1  22578  lgsquadlem2  22579  rpvmasumlem  22621  dchrisumlem1  22623  dchrisum0flblem1  22642  dchrisum0flblem2  22643  dchrisum0re  22647  dchrisum0lem1  22650  mudivsum  22664  mulogsum  22666  vmalogdivsum2  22672  logsqvma2  22677  selberg2lem  22684  logdivbnd  22690  selbergr  22702  selberg3r  22703  pntrlog2bndlem4  22714  pntrlog2bndlem5  22715  pntpbnd2  22721  ttgcontlem1  22954  brbtwn2  22974  colinearalglem4  22978  axsegconlem9  22994  ax5seglem1  22997  axbtwnid  23008  axeuclidlem  23031  axcontlem2  23034  axcontlem4  23036  grpoinvid1  23540  vcz  23771  hosubsub4  25045  lnop0  25193  branmfn  25332  difico  25896  omndmul2  25999  rdivmuldivd  26112  kerunit  26144  ballotlemfrceq  26759  ballotlemrinv0  26763  wrdsplex  26787  lgamgulmlem2  26864  lgamcvg2  26889  prodmolem3  27293  fallrisefac  27375  faclimlem1  27396  bpoly3  28048  mblfinlem2  28273  voliunnfl  28279  volsupnfl  28280  itg2addnclem3  28289  ftc2nc  28320  dvasin  28324  areacirclem1  28328  areacirclem4  28331  rngonegmn1l  28599  rngonegmn1r  28600  irrapxlem5  29012  pellfund14  29084  rmxdbl  29125  jm2.22  29189  dgrnznn  29337  itgpowd  29435  sigariz  29745  clwwlkel  30301  lfl0  32283  latmassOLD  32447  omlmod1i2N  32478  llnexchb2lem  33085  dalawlem3  33090  pmapj2N  33146  osumcllem9N  33181  pexmidlem6N  33192  4atexlemc  33286  cdleme1  33444  cdleme42a  33688  cdlemg13a  33868  cdlemh2  34033  cdlemk1  34048  tendocnv  34239  dihmeetlem12N  34536  dihmeetlem16N  34540  dihmeetlem19N  34543  dochsatshp  34669  dochexmidlem6  34683  mapdval4N  34850  mapdpglem28  34919  mapdpglem31  34921  mapdindp4  34941  hdmap14lem1a  35087  hdmapinvlem4  35142
  Copyright terms: Public domain W3C validator