Theorem 3eqtr3d 2279

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 2273	. 2 |- ( ph -> B = C )
4		3eqtr3d.3	. 2 |- ( ph -> B = D )
5	3, 4	eqtr3d 2273	1 |- ( ph -> C = D )

This proof depends on syntax axioms:   -> wi 4   = wceq 1402

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231

This theorem is used by:  mpteqb  5796  fvmptt  5797  fsnunfv  5916  f1ocnvfv1  5983  f1ocnvfv2  5984  fcof1  5989  caov12d  6271  caov13d  6273  caov411d  6275  caovimo  6283  tfrlem5  6585  tfrlemiubacc  6601  tfr1onlemubacc  6617  tfrcllemubacc  6630  nndir  6763  en2  7112  fopwdom  7136  updjud  7422  omp1eomlem  7434  addassnqg  7749  distrnqg  7754  enq0tr  7801  distrnq0  7826  distnq0r  7830  addnqprl  7896  addnqpru  7897  appdivnq  7930  ltmprr  8009  addcmpblnr  8106  mulcmpblnrlemg  8107  ltsrprg  8114  1idsr  8135  pn0sr  8138  mulgt0sr  8145  map2psrprg  8172  axmulass  8240  ax0id  8245  recriota  8257  mul12  8456  mul4  8459  readdcan  8467  add12  8485  cnegexlem2  8503  addcan  8507  ppncan  8569  addsub4  8570  subeqxfrd  8690  subaddeqd  8696  muladd  8712  mulcanapd  8991  receuap  9001  div13ap  9025  divdivdivap  9045  divcanap5  9046  divdivap1  9055  divdivap2  9056  halfaddsub  9543  lincmble  10416  fztp  10495  fseq1p1m1  10511  flqzadd  10746  flqdiv  10771  mulp1mod1  10815  modqnegd  10829  modqsub12d  10831  q2submod  10835  modsumfzodifsn  10846  seq3m1  10923  seq3caopr  10945  seqcaoprg  10946  iseqf1olemab  10952  iseqf1olemnanb  10953  seq3f1olemqsumk  10962  seqf1og  10971  exprecap  11030  expsubap  11037  zesq  11109  nn0opthlem1d  11172  facnn2  11186  faclbnd6  11196  bcm1n  11221  hashfibclem  11296  hashfac  11302  zfz1isolemsplit  11304  seq3coll  11308  ccatopth  11502  shftval3  11606  crre  11636  resub  11649  imsub  11657  cjsub  11671  sq01  11674  bdtrilem  12021  bdtri  12022  climshft2  12088  nnf1o  12159  fsumf1o  12173  isumss  12174  fisumss  12175  fsumadd  12189  isumclim3  12206  fsummulc2  12231  fsumsub  12235  telfsumo  12249  telfsumo2  12250  hashiun  12261  bcxmas  12272  isumshft  12273  trireciplem  12283  geoserap  12290  geo2sum2  12298  fprodf1o  12371  prodssdc  12372  fprodssdc  12373  fprodmul  12374  fprodm1  12381  sinsub  12523  cossub  12524  p1modz1  12577  bitsinv1lem  12744  bitsinv1  12745  gcdaddm  12777  modgcd  12784  bezoutlemnewy  12789  absmulgcd  12810  gcdmultiplez  12814  eucalg  12853  lcmgcd  12872  lcmid  12874  numdensq  12998  dfphi2  13018  phiprm  13021  fermltl  13032  prmdiveq  13034  hashgcdlem  13036  odzdvds  13044  powm2modprm  13051  modprm0  13053  coprimeprodsq  13056  pythagtriplem6  13069  pythagtriplem7  13070  pythagtriplem12  13074  pythagtriplem14  13076  pythagtriplem16  13078  pcaddlem  13138  sumhashdc  13146  fldivp1  13147  pcfac  13149  pockthlem  13155  4sqlem12  13201  4sqlem15  13204  ennnfonelem1  13347  ennnfonelemex  13354  topnpropgd  13656  qusaddvallemg  13703  grpinvalem  13754  grpinva  13755  grprida  13756  mnd12g  13790  resmhm  13843  grprcan  13891  grplcan  13916  grpasscan1  13917  grpinv11  13923  grpinvnz  13925  grplmulf1o  13928  grpinvpropdg  13929  grpinvadd  13932  grpsubsub4  13947  dfgrp3m  13953  imasgrp2  13962  mhmid  13967  mhmmnd  13968  mulgz  14002  mulgdirlem  14005  mulgdir  14006  mulgass  14011  mulgsubdir  14014  mulgpropdg  14016  isnsg3  14059  nmzsubg  14062  ssnmz  14063  eqger  14076  eqglact  14077  ghminv  14102  conjnmz  14131  ghmcmn  14180  gzsumconst  14192  gzsummhm2  14195  gsummhm2fi  14214  rnglz  14293  rngrz  14294  isrngd  14301  ringcom  14385  crngpropd  14393  isringd  14395  ringlz  14397  ringrz  14398  ring1eq0  14402  ringmneg1  14407  mulgass3  14440  unitgrp  14472  rngidpropdg  14502  invrpropdg  14505  isrhm2d  14521  rhmunitinv  14534  subrngpropd  14573  subrginv  14594  subrgunit  14596  subrgpropd  14610  rhmpropd  14611  unitrrg  14625  aprlring  14649  lmodvs0  14708  lmodvneg1  14716  lmodcom  14719  lmodsubdi  14730  lss0v  14816  lidlrsppropdg  14881  mulgrhm2  14994  znidomb  15042  asclpropd  15089  restin  15326  blpnfctr  15589  xmssym  15619  limcimolemlt  15814  dvmulxxbr  15852  dvrecap  15863  dvmptaddx  15869  dvmptmulx  15870  dvmptnegcn  15872  dvmptsubcn  15873  dvmptcjx  15874  dveflem  15876  plymullem1  15898  dvply1  15915  sin0pilem1  15932  ptolemy  15975  tangtx  15989  rpcxpneg  16062  rpcxpsub  16063  cxprec  16065  rpcxproot  16069  cxpcom  16093  rpabscxpbnd  16095  zprmlogbaplem3  16136  pellexlem2  16149  wilthlem1  16151  sgmppw  16187  1sgmprm  16189  1sgm2ppw  16190  ppiqub  16194  perfectlem1  16197  perfectlem2  16198  lgsvalmod  16236  lgsneg  16241  lgsdilem  16244  lgsne0  16255  lgssq  16257  lgssq2  16258  gausslemma2dlem1f1o  16277  gausslemma2dlem6  16284  gausslemma2d  16286  lgseisenlem1  16287  lgseisenlem2  16288  lgseisenlem4  16290  lgsquadlem1  16294  lgsquadlem3  16296  lgsquad3  16301  m1lgs  16302  p1evtxdeqfilem  16650  peano4nninf  17147  nninfalllem1  17149  nninfall  17150  nninfsellemqall  17156  qdencn  17170  qdiff  17196