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

Theorem 3eqtr3rd 2649
Description: A deduction from three chained equalities. (Contributed by NM, 14-Jan-2006.)
Hypotheses
Ref Expression
3eqtr3d.1 (𝜑𝐴 = 𝐵)
3eqtr3d.2 (𝜑𝐴 = 𝐶)
3eqtr3d.3 (𝜑𝐵 = 𝐷)
Assertion
Ref Expression
3eqtr3rd (𝜑𝐷 = 𝐶)

Proof of Theorem 3eqtr3rd
StepHypRef Expression
1 3eqtr3d.3 . 2 (𝜑𝐵 = 𝐷)
2 3eqtr3d.1 . . 3 (𝜑𝐴 = 𝐵)
3 3eqtr3d.2 . . 3 (𝜑𝐴 = 𝐶)
42, 3eqtr3d 2642 . 2 (𝜑𝐵 = 𝐶)
51, 4eqtr3d 2642 1 (𝜑𝐷 = 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1474
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-ext 2586
This theorem depends on definitions:  df-bi 195  df-cleq 2599
This theorem is referenced by:  iunxdif3  4533  fcofo  6418  fcof1oinvd  6423  cantnfp1lem3  8434  fin1a2lem7  9085  prlem934  9708  addid2  10067  addcom  10070  addcomd  10086  negeu  10119  add20  10386  2halves  11104  bcnn  12913  bcpasc  12922  hashfun  13033  wrdeqs1cat  13269  sqreulem  13890  summolem3  14235  fsumneg  14304  geolim  14383  geolim2  14384  mertens  14400  prodmolem3  14445  fallrisefac  14538  bpoly3  14571  sincossq  14688  demoivre  14712  eirrlem  14714  oddpwp1fsum  14896  sadeq  14975  gcdid  15029  phiprmpw  15262  pythagtriplem12  15312  expnprm  15387  fullresc  16277  grpinvid1  17236  grpnpcan  17273  grplactcnv  17284  ghmgrp  17305  conjghm  17457  odmodnn0  17725  gex1  17772  sylow3lem3  17810  efgredeu  17931  odadd2  18018  gsumval3  18074  pgpfac1lem3a  18241  ringnegl  18360  rngnegr  18361  ringmneg2  18363  lmodfopne  18667  lmodvsneg  18673  lss0v  18780  lssvs0or  18874  lvecinv  18877  lspabs2  18884  mplcoe3  19230  mplcoe5  19232  evlvar  19293  zringcyg  19598  zringunit  19600  mdetrlin  20166  mdetunilem6  20181  cramerimplem3  20249  cramerimp  20250  paste  20847  tuslem  21820  tususs  21823  ngpds  22155  ioo2bl  22333  ipcau2  22759  dvexp3  23459  rolle  23471  cmvth  23472  dv11cn  23482  lhop  23497  itgsubstlem  23529  ply1divex  23614  fta1glem1  23643  fta1g  23645  dgrnznn  23721  fta1  23781  vieta1lem2  23784  aaliou2  23813  dvtaylp  23842  dvntaylp  23843  taylthlem1  23845  taylthlem2  23846  dvradcnv  23893  ptolemy  23966  coskpi  23990  tanregt0  24003  cxpeq  24212  isosctrlem2  24263  chordthmlem  24273  dcubic  24287  quart1lem  24296  tanatan  24360  atantan  24364  dvatan  24376  birthdaylem2  24393  rlimcxp  24414  jensenlem2  24428  logdiflbnd  24435  emcllem2  24437  lgamgulmlem2  24470  lgamcvg2  24495  basellem8  24528  bclbnd  24719  lgsqr  24790  lgseisenlem3  24816  lgseisenlem4  24817  lgsquadlem1  24819  lgsquadlem2  24820  rpvmasumlem  24890  dchrisumlem1  24892  dchrisum0flblem1  24911  dchrisum0flblem2  24912  dchrisum0re  24916  dchrisum0lem1  24919  mudivsum  24933  mulogsum  24935  vmalogdivsum2  24941  logsqvma2  24946  selberg2lem  24953  logdivbnd  24959  selbergr  24971  selberg3r  24972  pntrlog2bndlem4  24983  pntrlog2bndlem5  24984  pntpbnd2  24990  miduniq  25295  krippenlem  25300  colperpexlem2  25338  ttgcontlem1  25480  brbtwn2  25500  colinearalglem4  25504  axsegconlem9  25520  ax5seglem1  25523  axbtwnid  25534  axeuclidlem  25557  axcontlem2  25560  axcontlem4  25562  clwwlkel  26084  grpoinvid1  26529  vcz  26588  hosubsub4  27864  lnop0  28012  branmfn  28151  difico  28738  omndmul2  28846  rdivmuldivd  28925  kerunit  28957  carsggect  29510  carsgclctunlem2  29511  ballotlemfrceq  29720  ballotlemrinv0  29724  wrdsplex  29747  faclimlem1  30685  poimirlem4  32383  poimirlem23  32402  mblfinlem2  32417  voliunnfl  32423  volsupnfl  32424  itg2addnclem3  32433  ftc2nc  32464  dvasin  32466  areacirclem1  32470  areacirclem4  32473  rngonegmn1l  32710  rngonegmn1r  32711  lfl0  33170  latmassOLD  33334  omlmod1i2N  33365  llnexchb2lem  33972  dalawlem3  33977  pmapj2N  34033  osumcllem9N  34068  pexmidlem6N  34079  4atexlemc  34173  cdleme1  34332  cdleme42a  34577  cdlemg13a  34757  cdlemh2  34922  cdlemk1  34937  tendocnv  35128  dihmeetlem12N  35425  dihmeetlem16N  35429  dihmeetlem19N  35432  dochsatshp  35558  dochexmidlem6  35572  mapdval4N  35739  mapdpglem28  35808  mapdpglem31  35810  mapdindp4  35830  hdmap14lem1a  35976  hdmapinvlem4  36031  irrapxlem5  36208  pellfund14  36280  rmxdbl  36322  jm2.22  36380  itgpowd  36619  0ellimcdiv  38517  fourierdlem95  38895  etransclem46  38974  sigariz  39502  clwwlksel  41220  altgsumbc  41922  blengt1fldiv2p1  42184
  Copyright terms: Public domain W3C validator