Theorem 3eqtr3d 2218

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	⊢ (𝜑 → 𝐴 = 𝐵)
3eqtr3d.2	⊢ (𝜑 → 𝐴 = 𝐶)
3eqtr3d.3	⊢ (𝜑 → 𝐵 = 𝐷)

Assertion

Ref	Expression
3eqtr3d	⊢ (𝜑 → 𝐶 = 𝐷)

Proof of Theorem 3eqtr3d

Step	Hyp	Ref	Expression
1		3eqtr3d.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
2		3eqtr3d.2	. . 3 ⊢ (𝜑 → 𝐴 = 𝐶)
3	1, 2	eqtr3d 2212	. 2 ⊢ (𝜑 → 𝐵 = 𝐶)
4		3eqtr3d.3	. 2 ⊢ (𝜑 → 𝐵 = 𝐷)
5	3, 4	eqtr3d 2212	1 ⊢ (𝜑 → 𝐶 = 𝐷)

Syntax hints:   → wi 4   = wceq 1353

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1447  ax-gen 1449  ax-4 1510  ax-17 1526  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-cleq 2170

This theorem is referenced by:  mpteqb  5606  fvmptt  5607  fsnunfv  5717  f1ocnvfv1  5777  f1ocnvfv2  5778  fcof1  5783  caov12d  6055  caov13d  6057  caov411d  6059  caovimo  6067  tfrlem5  6314  tfrlemiubacc  6330  tfr1onlemubacc  6346  tfrcllemubacc  6359  nndir  6490  fopwdom  6835  updjud  7080  omp1eomlem  7092  addassnqg  7380  distrnqg  7385  enq0tr  7432  distrnq0  7457  distnq0r  7461  addnqprl  7527  addnqpru  7528  appdivnq  7561  ltmprr  7640  addcmpblnr  7737  mulcmpblnrlemg  7738  ltsrprg  7745  1idsr  7766  pn0sr  7769  mulgt0sr  7776  map2psrprg  7803  axmulass  7871  ax0id  7876  recriota  7888  mul12  8085  mul4  8088  readdcan  8096  add12  8114  cnegexlem2  8132  addcan  8136  ppncan  8198  addsub4  8199  subeqxfrd  8319  subaddeqd  8325  muladd  8340  mulcanapd  8617  receuap  8625  div13ap  8649  divdivdivap  8669  divcanap5  8670  divdivap1  8679  divdivap2  8680  halfaddsub  9152  fztp  10077  fseq1p1m1  10093  flqzadd  10297  flqdiv  10320  mulp1mod1  10364  modqnegd  10378  modqsub12d  10380  q2submod  10384  modsumfzodifsn  10395  seq3m1  10467  seq3caopr  10482  iseqf1olemab  10488  iseqf1olemnanb  10489  seq3f1olemqsumk  10498  exprecap  10560  expsubap  10567  zesq  10638  nn0opthlem1d  10699  facnn2  10713  faclbnd6  10723  zfz1isolemsplit  10817  seq3coll  10821  shftval3  10835  crre  10865  resub  10878  imsub  10886  cjsub  10900  bdtrilem  11246  bdtri  11247  climshft2  11313  nnf1o  11383  fsumf1o  11397  isumss  11398  fisumss  11399  fsumadd  11413  isumclim3  11430  fsummulc2  11455  fsumsub  11459  telfsumo  11473  telfsumo2  11474  hashiun  11485  bcxmas  11496  isumshft  11497  trireciplem  11507  geoserap  11514  geo2sum2  11522  fprodf1o  11595  prodssdc  11596  fprodssdc  11597  fprodmul  11598  fprodm1  11605  sinsub  11747  cossub  11748  p1modz1  11800  gcdaddm  11984  modgcd  11991  bezoutlemnewy  11996  absmulgcd  12017  gcdmultiplez  12021  eucalg  12058  lcmgcd  12077  lcmid  12079  numdensq  12201  dfphi2  12219  phiprm  12222  fermltl  12233  prmdiveq  12235  hashgcdlem  12237  odzdvds  12244  powm2modprm  12251  modprm0  12253  coprimeprodsq  12256  pythagtriplem6  12269  pythagtriplem7  12270  pythagtriplem12  12274  pythagtriplem14  12276  pythagtriplem16  12278  pcaddlem  12337  sumhashdc  12344  fldivp1  12345  pcfac  12347  pockthlem  12353  ennnfonelem1  12407  ennnfonelemex  12414  topnpropgd  12701  qusaddvallemg  12751  grprinvlem  12803  grprinvd  12804  grpridd  12805  mnd12g  12828  grprcan  12909  grplcan  12931  grpasscan1  12932  grpinv11  12938  grpinvnz  12940  grplmulf1o  12943  grpinvpropdg  12944  grpinvadd  12947  grpsubsub4  12962  dfgrp3m  12968  mhmid  12978  mhmmnd  12979  mulgz  13009  mulgdirlem  13012  mulgdir  13013  mulgass  13018  mulgsubdir  13021  mulgpropdg  13023  isnsg3  13065  nmzsubg  13068  ssnmz  13069  eqger  13081  eqglact  13082  ringcom  13212  crngpropd  13216  isringd  13218  ringlz  13220  ringrz  13221  ring1eq0  13223  ringmneg1  13228  mulgass3  13252  unitgrp  13283  rngidpropdg  13313  invrpropdg  13316  subrginv  13356  subrgunit  13358  subrgpropd  13367  restin  13646  blpnfctr  13909  xmssym  13939  limcimolemlt  14103  dvmulxxbr  14136  dvrecap  14147  dvmptaddx  14151  dvmptmulx  14152  dvmptnegcn  14154  dvmptsubcn  14155  dvmptcjx  14156  dveflem  14157  sin0pilem1  14172  ptolemy  14215  tangtx  14229  rpcxpneg  14298  rpcxpsub  14299  cxprec  14301  rpcxproot  14304  cxpcom  14327  rpabscxpbnd  14329  lgsvalmod  14390  lgsneg  14395  lgsdilem  14398  lgsne0  14409  lgssq  14411  lgssq2  14412  lgseisenlem1  14420  lgseisenlem2  14421  m1lgs  14422  peano4nninf  14725  nninfalllem1  14727  nninfall  14728  nninfsellemqall  14734  qdencn  14745