Theorem 3eqtr2rd 2775

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
3eqtr2rd	⊢ (𝜑 → 𝐷 = 𝐴)

Proof of Theorem 3eqtr2rd

Step	Hyp	Ref	Expression
1		3eqtr2d.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
2		3eqtr2d.2	. . 3 ⊢ (𝜑 → 𝐶 = 𝐵)
3	1, 2	eqtr4d 2771	. 2 ⊢ (𝜑 → 𝐴 = 𝐶)
4		3eqtr2d.3	. 2 ⊢ (𝜑 → 𝐶 = 𝐷)
5	3, 4	eqtr2d 2769	1 ⊢ (𝜑 → 𝐷 = 𝐴)

Syntax hints:   → wi 4   = wceq 1541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2725

This theorem is referenced by:  nneob  8577  xp1d2m1eqxm1d2  12382  negmod  13825  modeqmodmin  13850  faclbnd2  14200  cats1un  14630  cjmulval  15054  fsumsplit  15650  fzosump1  15661  bcxmas  15744  trireciplem  15771  geo2sum  15782  geo2lim  15784  geoisum1c  15789  mertenslem1  15793  fprodsplit  15875  risefallfac  15933  bpolydiflem  15963  eftlub  16020  tanadd  16078  addsin  16081  subsin  16082  subcos  16086  sadadd2lem2  16363  qredeu  16571  zsqrtelqelz  16671  4sqlem15  16873  rcaninv  17703  resssetc  18001  resscatc  18018  curfcl  18140  mulgaddcomlem  19012  conjghm  19163  gasubg  19216  dfod2  19478  efginvrel2  19641  efgcpbllemb  19669  odadd2  19763  frgpnabllem1  19787  srgbinomlem3  20148  pws1  20245  prdslmodd  20904  znunithash  21503  frlmipval  21718  frlmlbs  21736  psrlmod  21898  restcld  23088  clmneg  25009  rrxds  25321  itg2monolem1  25679  itgconst  25748  dvexp  25885  dvfsumabs  25957  dvtaylp  26306  taylthlem2  26310  taylthlem2OLD  26311  tangtx  26442  logsqrt  26641  zrtelqelz  26696  lawcoslem1  26753  chordthmlem2  26771  chordthmlem4  26773  tanatan  26857  atanbndlem  26863  amgmlem  26928  basellem3  27021  basellem5  27023  mpodvdsmulf1o  27132  dvdsmulf1o  27134  chtub  27151  fsumvma  27152  lgsquad2lem1  27323  2sqlem8  27365  dchrmusum2  27433  logsqvma  27481  pntrlog2bndlem4  27519  pw2divsnegd  28373  miriso  28649  lmieu  28763  ttgcontlem1  28864  brbtwn2  28885  ax5seglem1  28908  axcontlem2  28945  axcontlem4  28947  clwwlkel  30028  vc0  30556  hvsubdistr2  31032  adjlnop  32068  adjcoi  32082  cnvbraval  32092  fpwrelmap  32720  fsumiunle  32817  xrge0adddir  33006  cycpm2tr  33095  cycpmco2lem4  33105  cycpmco2lem7  33108  cyc3genpmlem  33127  archirngz  33165  archiabllem1b  33168  erler  33239  qusrn  33381  ressply10g  33537  ply1gsumz  33566  fedgmullem1  33663  fedgmullem2  33664  dimlssid  33666  constrrtcc  33769  rspectopn  33901  xrge0pluscn  33974  esumfzf  34103  esumiun  34128  volmeas  34265  omssubadd  34334  breprexplemc  34666  bnj553  34931  cvmliftlem6  35355  cvmliftlem10  35359  cvmlift2lem3  35370  finxpreclem4  37459  sin2h  37670  matunitlindflem2  37677  poimirlem16  37696  heibor  37881  ghomdiv  37952  3atlem1  39602  atmod3i2  39984  trljat2  40286  cdleme1  40346  cdleme22eALTN  40464  cdlemh2  40935  dihglblem3N  41414  dih1dimatlem0  41447  djhlsmcl  41533  mapdpglem30  41821  hdmapneg  41965  hgmapval1  42012  hgmapmul  42014  sn-1ne2  42383  sn-addrid  42539  fltnltalem  42780  3cubeslem3r  42804  3cubeslem4  42806  proot1ex  43313  tfsconcatfv  43458  dirkerper  46218  fourierdlem83  46311  fourierdlem92  46320  sigarperm  46982  sigaradd  46988  fmtnorec1  47661  lincresunit3lem2  48605  itsclc0yqsollem1  48887  itsclinecirc0b  48899  fuco11bALT  49463  prstchomval  49684  sinhpcosh  49865  amgmwlem  49927