Theorem 3eqtr3d 2180

Description: A deduction from three chained equalities. (Contributed by NM, 4-Aug-1995.) (Proof shortened by Andrew Salmon, 25-May-2011.)

Hypotheses

Ref	Expression
3eqtr3d.1	|- ( ph -> A = B )
3eqtr3d.2	|- ( ph -> A = C )
3eqtr3d.3	|- ( ph -> B = D )

Assertion

Ref	Expression
3eqtr3d	|- ( ph -> C = D )

Proof of Theorem 3eqtr3d

Step	Hyp	Ref	Expression
1		3eqtr3d.1	. . 3 |- ( ph -> A = B )
2		3eqtr3d.2	. . 3 |- ( ph -> A = C )
3	1, 2	eqtr3d 2174	. 2 |- ( ph -> B = C )
4		3eqtr3d.3	. 2 |- ( ph -> B = D )
5	3, 4	eqtr3d 2174	1 |- ( ph -> C = D )

Syntax hints:   -> wi 4   = wceq 1331

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-gen 1425  ax-4 1487  ax-17 1506  ax-ext 2121

This theorem depends on definitions:  df-bi 116  df-cleq 2132

This theorem is referenced by:  mpteqb  5511  fvmptt  5512  fsnunfv  5621  f1ocnvfv1  5678  f1ocnvfv2  5679  fcof1  5684  caov12d  5952  caov13d  5954  caov411d  5956  caovimo  5964  grprinvlem  5965  grprinvd  5966  grpridd  5967  tfrlem5  6211  tfrlemiubacc  6227  tfr1onlemubacc  6243  tfrcllemubacc  6256  nndir  6386  fopwdom  6730  updjud  6967  omp1eomlem  6979  addassnqg  7190  distrnqg  7195  enq0tr  7242  distrnq0  7267  distnq0r  7271  addnqprl  7337  addnqpru  7338  appdivnq  7371  ltmprr  7450  addcmpblnr  7547  mulcmpblnrlemg  7548  ltsrprg  7555  1idsr  7576  pn0sr  7579  mulgt0sr  7586  map2psrprg  7613  axmulass  7681  ax0id  7686  recriota  7698  mul12  7891  mul4  7894  readdcan  7902  add12  7920  cnegexlem2  7938  addcan  7942  ppncan  8004  addsub4  8005  subeqxfrd  8125  subaddeqd  8131  muladd  8146  mulcanapd  8422  receuap  8430  div13ap  8453  divdivdivap  8473  divcanap5  8474  divdivap1  8483  divdivap2  8484  halfaddsub  8954  fztp  9858  fseq1p1m1  9874  flqzadd  10071  flqdiv  10094  mulp1mod1  10138  modqnegd  10152  modqsub12d  10154  q2submod  10158  modsumfzodifsn  10169  seq3m1  10241  seq3caopr  10256  iseqf1olemab  10262  iseqf1olemnanb  10263  seq3f1olemqsumk  10272  exprecap  10334  expsubap  10341  zesq  10410  nn0opthlem1d  10466  facnn2  10480  faclbnd6  10490  zfz1isolemsplit  10581  seq3coll  10585  shftval3  10599  crre  10629  resub  10642  imsub  10650  cjsub  10664  bdtrilem  11010  bdtri  11011  climshft2  11075  nnf1o  11145  fsumf1o  11159  isumss  11160  fisumss  11161  fsumadd  11175  isumclim3  11192  fsummulc2  11217  fsumsub  11221  telfsumo  11235  telfsumo2  11236  hashiun  11247  bcxmas  11258  isumshft  11259  trireciplem  11269  geoserap  11276  geo2sum2  11284  sinsub  11447  cossub  11448  gcdaddm  11672  modgcd  11679  bezoutlemnewy  11684  absmulgcd  11705  gcdmultiplez  11709  eucalg  11740  lcmgcd  11759  lcmid  11761  numdensq  11880  dfphi2  11896  phiprm  11899  hashgcdlem  11903  ennnfonelem1  11920  ennnfonelemex  11927  topnpropgd  12134  restin  12345  blpnfctr  12608  xmssym  12638  limcimolemlt  12802  dvmulxxbr  12835  dvrecap  12846  dvmptaddx  12850  dvmptmulx  12851  dvmptnegcn  12853  dvmptsubcn  12854  dveflem  12855  sin0pilem1  12862  ptolemy  12905  tangtx  12919  peano4nninf  13200  nninfalllem1  13203  nninfall  13204  nninfsellemqall  13211  qdencn  13222