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

Theorem 3eqtr3rd 2517
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 2510 . 2  |-  ( ph  ->  B  =  C )
51, 4eqtr3d 2510 1  |-  ( ph  ->  D  =  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1379
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-cleq 2459
This theorem is referenced by:  fcofo  6177  fcof1oinvd  6182  cantnfp1lem3  8095  cantnfp1lem3OLD  8121  fin1a2lem7  8782  prlem934  9407  addid2  9758  addcom  9761  addcomd  9777  negeu  9806  add20  10060  2halves  10763  bcnn  12354  bcpasc  12363  hashfun  12457  wrdeqs1cat  12659  sqreulem  13151  summolem3  13495  fsumneg  13561  geolim  13638  geolim2  13639  mertens  13654  sincossq  13768  demoivre  13792  eirrlem  13794  sadeq  13977  gcdid  14024  phiprmpw  14161  pythagtriplem12  14205  expnprm  14276  fullresc  15074  grpinvid1  15899  grpnpcan  15931  grplactcnv  15939  conjghm  16092  odmodnn0  16360  gex1  16407  sylow3lem3  16445  efgredeu  16566  odadd2  16648  gsumval3OLD  16699  gsumval3  16702  pgpfac1lem3a  16917  rngnegl  17026  rngnegr  17027  rngmneg2  17029  lmodvsneg  17337  lss0v  17445  lssvs0or  17539  lvecinv  17542  lspabs2  17549  mplcoe3  17899  mplcoe3OLD  17900  mplcoe5  17902  mplcoe2OLD  17904  evlvar  17969  zringcyg  18280  zcyg  18285  zringunit  18287  zrngunit  18288  mdetrlin  18871  mdetunilem6  18886  cramerimplem3  18954  cramerimp  18955  paste  19561  tuslem  20505  tususs  20508  ngpds  20858  ioo2bl  21033  ipcau2  21412  cmetcusp  21529  dvexp3  22114  rolle  22126  cmvth  22127  dv11cn  22137  lhop  22152  itgsubstlem  22184  ply1divex  22272  fta1glem1  22301  fta1g  22303  fta1  22438  vieta1lem2  22441  aaliou2  22470  dvtaylp  22499  dvntaylp  22500  taylthlem1  22502  taylthlem2  22503  dvradcnv  22550  ptolemy  22622  coskpi  22646  tanregt0  22659  cxpeq  22859  isosctrlem2  22881  chordthmlem  22891  dcubic  22905  quart1lem  22914  tanatan  22978  atantan  22982  dvatan  22994  birthdaylem2  23010  rlimcxp  23031  jensenlem2  23045  logdiflbnd  23052  emcllem2  23054  basellem8  23089  bclbnd  23283  lgsqr  23349  lgseisenlem3  23354  lgseisenlem4  23355  lgsquadlem1  23357  lgsquadlem2  23358  rpvmasumlem  23400  dchrisumlem1  23402  dchrisum0flblem1  23421  dchrisum0flblem2  23422  dchrisum0re  23426  dchrisum0lem1  23429  mudivsum  23443  mulogsum  23445  vmalogdivsum2  23451  logsqvma2  23456  selberg2lem  23463  logdivbnd  23469  selbergr  23481  selberg3r  23482  pntrlog2bndlem4  23493  pntrlog2bndlem5  23494  pntpbnd2  23500  miduniq2  23772  krippenlem  23775  colperpexlem2  23810  ttgcontlem1  23864  brbtwn2  23884  colinearalglem4  23888  axsegconlem9  23904  ax5seglem1  23907  axbtwnid  23918  axeuclidlem  23941  axcontlem2  23944  axcontlem4  23946  clwwlkel  24469  grpoinvid1  24908  vcz  25139  hosubsub4  26413  lnop0  26561  branmfn  26700  difico  27262  omndmul2  27364  rdivmuldivd  27444  kerunit  27476  ballotlemfrceq  28107  ballotlemrinv0  28111  wrdsplex  28135  lgamgulmlem2  28212  lgamcvg2  28237  prodmolem3  28642  fallrisefac  28724  faclimlem1  28745  bpoly3  29397  mblfinlem2  29629  voliunnfl  29635  volsupnfl  29636  itg2addnclem3  29645  ftc2nc  29676  dvasin  29680  areacirclem1  29684  areacirclem4  29687  rngonegmn1l  29955  rngonegmn1r  29956  irrapxlem5  30366  pellfund14  30438  rmxdbl  30479  jm2.22  30541  dgrnznn  30689  itgpowd  30787  sigariz  31547  altgsumbc  32005  lfl0  33862  latmassOLD  34026  omlmod1i2N  34057  llnexchb2lem  34664  dalawlem3  34669  pmapj2N  34725  osumcllem9N  34760  pexmidlem6N  34771  4atexlemc  34865  cdleme1  35023  cdleme42a  35267  cdlemg13a  35447  cdlemh2  35612  cdlemk1  35627  tendocnv  35818  dihmeetlem12N  36115  dihmeetlem16N  36119  dihmeetlem19N  36122  dochsatshp  36248  dochexmidlem6  36262  mapdval4N  36429  mapdpglem28  36498  mapdpglem31  36500  mapdindp4  36520  hdmap14lem1a  36666  hdmapinvlem4  36721
  Copyright terms: Public domain W3C validator