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

Theorem 3eqtr2d 2842
Description: A deduction from three chained equalities. (Contributed by NM, 4-Aug-2006.)
Hypotheses
Ref Expression
3eqtr2d.1 (𝜑𝐴 = 𝐵)
3eqtr2d.2 (𝜑𝐶 = 𝐵)
3eqtr2d.3 (𝜑𝐶 = 𝐷)
Assertion
Ref Expression
3eqtr2d (𝜑𝐴 = 𝐷)

Proof of Theorem 3eqtr2d
StepHypRef Expression
1 3eqtr2d.1 . . 3 (𝜑𝐴 = 𝐵)
2 3eqtr2d.2 . . 3 (𝜑𝐶 = 𝐵)
31, 2eqtr4d 2839 . 2 (𝜑𝐴 = 𝐶)
4 3eqtr2d.3 . 2 (𝜑𝐶 = 𝐷)
53, 4eqtrd 2836 1 (𝜑𝐴 = 𝐷)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1538
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2122  ax-ext 2773
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2794
This theorem is referenced by:  fmptapd  6914  negsub  10927  neg2sub  10939  divmuleq  11338  divneg2  11357  discr  13601  bcpasc  13681  hashgval2  13739  hashf1lem2  13814  relexpaddnn  14406  crim  14470  remullem  14483  isum1p  15192  geo2sum  15225  fallfacfwd  15386  fsumkthpow  15406  bpoly3  15408  bpoly4  15409  efi4p  15486  sinhval  15503  addcos  15523  cos2tsin  15528  demoivreALT  15550  rpnnen2lem11  15573  omeo  15711  pwp1fsum  15736  sadaddlem  15809  bitsres  15816  smumullem  15835  sqgcd  15903  eulerthlem2  16113  vfermltlALT  16133  pockthlem  16235  4sqlem10  16277  vdwlem2  16312  vdwlem6  16316  vdwlem8  16318  fuccocl  17230  resssetc  17348  resscatc  17361  uncfcurf  17485  yonedalem3b  17525  prdspjmhm  17989  grpinvid2  18151  imasgrp2  18210  mulgaddcomlem  18246  mulgmodid  18262  lagsubg2  18337  cntzsubm  18462  sylow3lem2  18749  efgredleme  18865  ablsubsub  18935  ablsubsub4  18936  odadd2  18966  gex2abl  18968  pgpfac1lem3a  19195  abvneg  19602  lmodfopne  19669  lsppr  19862  gzrngunit  20161  frlmsubgval  20458  frlmgsum  20465  psrass1  20647  resspsradd  20658  resspsrvsca  20660  mplcoe5  20712  mplmon2mul  20744  evlslem2  20755  evlsvarsrng  20775  coe1tm  20906  ply1scl1  20925  evls1varsrng  20968  mamuass  21011  mavmulass  21158  mulmarep1gsum2  21183  mdetuni0  21230  maducoeval2  21249  madulid  21254  mat2pmatmul  21340  decpmatmulsumfsupp  21382  pmatcollpwlem  21389  pm2mpmhmlem1  21427  cmpfi  22017  cnconn  22031  txrest  22240  utopsnneiplem  22857  blcvx  23407  tcphcphlem2  23844  cphipval2  23849  cphipval  23851  rrx0  24005  minveclem2  24034  pjthlem1  24045  uniioovol  24187  uniioombllem2  24191  itg1addlem4  24307  mbfi1fseqlem5  24327  itg2mulc  24355  itg2monolem1  24358  itgaddlem1  24430  itgmulc2lem2  24440  dvrec  24562  lhop2  24622  ftc1lem5  24647  deg1submon1p  24757  plypf1  24813  coefv0  24849  coemulhi  24855  coemulc  24856  dgreq0  24866  dvply1  24884  vieta1  24912  aareccl  24926  aaliou3lem8  24945  dvtaylp  24969  mtest  25003  sineq0  25120  efif1olem2  25139  efif1olem4  25141  tanarg  25214  logtayl2  25257  nnlogbexp  25371  isosctrlem2  25409  chordthmlem2  25423  chordthmlem4  25425  heron  25428  dcubic1lem  25433  dcubic1  25435  mcubic  25437  dquart  25443  quart1lem  25445  quart1  25446  efiasin  25478  asinsin  25482  atancj  25500  efiatan  25502  atanlogaddlem  25503  cosatan  25511  atantan  25513  atans2  25521  log2cnv  25534  log2tlbnd  25535  birthdaylem2  25542  cxplim  25561  lgamgulmlem2  25619  wilthlem1  25657  basellem3  25672  musum  25780  musumsum  25781  muinv  25782  pclogsum  25803  mersenne  25815  dchrabs  25848  dchrinv  25849  lgseisenlem1  25963  lgsquadlem1  25968  lgsquadlem2  25969  lgsquadlem3  25970  lgsquad2lem1  25972  2lgslem1  25982  2sqmod  26024  chebbnd1lem3  26059  chpchtlim  26067  rplogsumlem2  26073  dchrisumlem2  26078  dchrmusum2  26082  mulog2sumlem1  26122  mulog2sumlem3  26124  vmalogdivsum2  26126  selberg4lem1  26148  pntrlog2bndlem2  26166  pntrlog2bndlem4  26168  pntibndlem2  26179  pntlemr  26190  pntlemf  26193  pntlemo  26195  ragcom  26496  colperpexlem1  26528  lmiisolem  26594  hypcgrlem2  26598  trgcopyeulem  26603  brbtwn2  26703  colinearalglem1  26704  colinearalglem2  26705  axcontlem2  26763  axcontlem8  26769  numedglnl  26941  clwlkclwwlklem2a  27787  numclwlk1lem1  28158  numclwlk1lem2  28159  numclwwlk2  28170  grpoinvid2  28316  ablodivdiv4  28341  smcnlem  28484  ipidsq  28497  ipasslem2  28619  minvecolem2  28662  hv2times  28848  pjhthlem1  29178  pjds3i  29500  ho2times  29606  opsqrlem6  29932  pjclem4  29986  pj3si  29994  csmdsymi  30121  ofoprabco  30431  fcnvgreu  30440  swrdrndisj  30661  trsp2cyc  30819  cycpmco2lem3  30824  cycpmco2lem4  30825  cycpmco2lem5  30826  cycpmco2lem6  30827  cycpmco2  30829  imaslmod  30977  frlmdim  31101  rrxdim  31104  lbsdiflsp0  31114  fedgmullem1  31117  fedgmullem2  31118  extdg1id  31145  ccfldextdgrr  31149  qqhcn  31346  esumpr2  31440  esumpfinval  31448  esumpfinvalf  31449  carsggect  31690  oddpwdcv  31727  eulerpartlemgs2  31752  fibp1  31773  orvcelval  31840  ballotlemscr  31890  ballotlemfrci  31899  signsplypnf  31934  reprpmtf1o  32011  breprexplemc  32017  breprexp  32018  circlemeth  32025  lpadright  32069  revwlk  32485  subfacp1lem5  32545  cvmliftlem10  32655  circum  33031  faclimlem3  33091  fwddifnp1  33740  bj-bary1lem  34725  tan2h  35048  poimirlem3  35059  poimirlem13  35069  poimirlem14  35070  itgaddnclem1  35114  itgmulc2nclem2  35123  areacirclem1  35144  areacirclem4  35147  istotbnd3  35208  iscringd  35435  3atlem1  36778  pmod2iN  37144  polval2N  37201  lhple  37337  cdleme2  37523  cdleme35d  37747  cdleme42h  37777  cdlemeg46ngfr  37813  cdlemkid1  38217  lcfl7lem  38794  mapdpglem22  38988  mapdh6dN  39034  hdmap1l6d  39108  hdmapinvlem3  39215  lcmineqlem3  39318  nnadddir  39464  expgcd  39484  readdsub  39515  sn-negex12  39546  prjspeclsp  39599  3cubeslem3r  39621  diophin  39706  irrapxlem2  39757  pellexlem6  39768  pell1234qrmulcl  39789  rmxyval  39849  rmxyneg  39854  rmxyadd  39855  jm2.24  39897  jm2.25  39933  snhesn  40480  scottrankd  40949  radcnvrat  41011  binomcxplemnotnn0  41053  sub2times  41898  mul13d  41903  fperiodmullem  41928  fperiodmul  41929  isumneg  42237  climneg  42245  itgsinexp  42590  stoweidlem13  42648  stoweidlem42  42677  wallispilem4  42703  wallispilem5  42704  wallispi2lem1  42706  stirlinglem1  42709  stirlinglem3  42711  stirlinglem4  42712  stirlinglem5  42713  stirlinglem7  42715  stirlinglem10  42718  dirkertrigeqlem3  42735  fourierdlem30  42772  fourierdlem32  42774  fourierdlem42  42784  fourierdlem48  42789  fourierdlem49  42790  fourierdlem83  42824  sqwvfoura  42863  sqwvfourb  42864  etransclem2  42871  etransclem46  42915  sharhght  43472  imasetpreimafvbijlemfv  43912  fmtnorec3  44058  quad1  44131  requad1  44133  isomgreqve  44336  ushrisomgr  44352  rngcid  44596  ringcid  44642  lmodvsmdi  44777  dmatALTbas  44803  ldepsprlem  44874  itcovalt2lem2lem2  45081  ackval3  45090  1subrec1sub  45112  eenglngeehlnmlem1  45144  eenglngeehlnmlem2  45145  itsclc0xyqsolr  45176  sinhpcosh  45259
  Copyright terms: Public domain W3C validator