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

Syntax hints:   → wi 4   = wceq 1402

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 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

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

This theorem is referenced by:  mpteqb  5790  fvmptt  5791  fsnunfv  5907  f1ocnvfv1  5973  f1ocnvfv2  5974  fcof1  5979  caov12d  6261  caov13d  6263  caov411d  6265  caovimo  6273  tfrlem5  6575  tfrlemiubacc  6591  tfr1onlemubacc  6607  tfrcllemubacc  6620  nndir  6753  en2  7102  fopwdom  7126  updjud  7412  omp1eomlem  7424  addassnqg  7739  distrnqg  7744  enq0tr  7791  distrnq0  7816  distnq0r  7820  addnqprl  7886  addnqpru  7887  appdivnq  7920  ltmprr  7999  addcmpblnr  8096  mulcmpblnrlemg  8097  ltsrprg  8104  1idsr  8125  pn0sr  8128  mulgt0sr  8135  map2psrprg  8162  axmulass  8230  ax0id  8235  recriota  8247  mul12  8445  mul4  8448  readdcan  8456  add12  8474  cnegexlem2  8492  addcan  8496  ppncan  8558  addsub4  8559  subeqxfrd  8679  subaddeqd  8685  muladd  8701  mulcanapd  8979  receuap  8989  div13ap  9013  divdivdivap  9033  divcanap5  9034  divdivap1  9043  divdivap2  9044  halfaddsub  9518  lincmble  10385  fztp  10463  fseq1p1m1  10479  flqzadd  10711  flqdiv  10736  mulp1mod1  10780  modqnegd  10794  modqsub12d  10796  q2submod  10800  modsumfzodifsn  10811  seq3m1  10888  seq3caopr  10910  seqcaoprg  10911  iseqf1olemab  10917  iseqf1olemnanb  10918  seq3f1olemqsumk  10927  seqf1og  10936  exprecap  10995  expsubap  11002  zesq  11074  nn0opthlem1d  11136  facnn2  11150  faclbnd6  11160  bcm1n  11185  hashfibclem  11260  hashfac  11266  zfz1isolemsplit  11268  seq3coll  11272  ccatopth  11466  shftval3  11570  crre  11600  resub  11613  imsub  11621  cjsub  11635  sq01  11638  bdtrilem  11983  bdtri  11984  climshft2  12050  nnf1o  12121  fsumf1o  12135  isumss  12136  fisumss  12137  fsumadd  12151  isumclim3  12168  fsummulc2  12193  fsumsub  12197  telfsumo  12211  telfsumo2  12212  hashiun  12223  bcxmas  12234  isumshft  12235  trireciplem  12245  geoserap  12252  geo2sum2  12260  fprodf1o  12333  prodssdc  12334  fprodssdc  12335  fprodmul  12336  fprodm1  12343  sinsub  12485  cossub  12486  p1modz1  12539  bitsinv1lem  12706  bitsinv1  12707  gcdaddm  12739  modgcd  12746  bezoutlemnewy  12751  absmulgcd  12772  gcdmultiplez  12776  eucalg  12815  lcmgcd  12834  lcmid  12836  numdensq  12958  dfphi2  12976  phiprm  12979  fermltl  12990  prmdiveq  12992  hashgcdlem  12994  odzdvds  13002  powm2modprm  13009  modprm0  13011  coprimeprodsq  13014  pythagtriplem6  13027  pythagtriplem7  13028  pythagtriplem12  13032  pythagtriplem14  13034  pythagtriplem16  13036  pcaddlem  13096  sumhashdc  13104  fldivp1  13105  pcfac  13107  pockthlem  13113  4sqlem12  13159  4sqlem15  13162  ennnfonelem1  13276  ennnfonelemex  13283  topnpropgd  13584  qusaddvallemg  13631  grpinvalem  13682  grpinva  13683  grprida  13684  mnd12g  13718  resmhm  13771  grprcan  13819  grplcan  13844  grpasscan1  13845  grpinv11  13851  grpinvnz  13853  grplmulf1o  13856  grpinvpropdg  13857  grpinvadd  13860  grpsubsub4  13875  dfgrp3m  13881  imasgrp2  13890  mhmid  13895  mhmmnd  13896  mulgz  13930  mulgdirlem  13933  mulgdir  13934  mulgass  13939  mulgsubdir  13942  mulgpropdg  13944  isnsg3  13987  nmzsubg  13990  ssnmz  13991  eqger  14004  eqglact  14005  ghminv  14030  conjnmz  14059  ghmcmn  14108  gzsumconst  14120  gzsummhm2  14123  gsummhm2fi  14142  rnglz  14219  rngrz  14220  isrngd  14227  ringcom  14309  crngpropd  14317  isringd  14319  ringlz  14321  ringrz  14322  ring1eq0  14326  ringmneg1  14331  mulgass3  14364  unitgrp  14396  rngidpropdg  14426  invrpropdg  14429  isrhm2d  14445  rhmunitinv  14458  subrngpropd  14497  subrginv  14518  subrgunit  14520  subrgpropd  14534  rhmpropd  14535  unitrrg  14549  aprlring  14573  lmodvs0  14631  lmodvneg1  14639  lmodcom  14642  lmodsubdi  14653  lss0v  14739  lidlrsppropdg  14804  mulgrhm2  14917  znidomb  14965  restin  15200  blpnfctr  15463  xmssym  15493  limcimolemlt  15688  dvmulxxbr  15726  dvrecap  15737  dvmptaddx  15743  dvmptmulx  15744  dvmptnegcn  15746  dvmptsubcn  15747  dvmptcjx  15748  dveflem  15750  plymullem1  15772  dvply1  15789  sin0pilem1  15805  ptolemy  15848  tangtx  15862  rpcxpneg  15932  rpcxpsub  15933  cxprec  15935  rpcxproot  15939  cxpcom  15963  rpabscxpbnd  15965  pellexlem2  16006  wilthlem1  16008  sgmppw  16020  1sgmprm  16022  1sgm2ppw  16023  perfectlem1  16027  perfectlem2  16028  lgsvalmod  16052  lgsneg  16057  lgsdilem  16060  lgsne0  16071  lgssq  16073  lgssq2  16074  gausslemma2dlem1f1o  16093  gausslemma2dlem6  16100  gausslemma2d  16102  lgseisenlem1  16103  lgseisenlem2  16104  lgseisenlem4  16106  lgsquadlem1  16110  lgsquadlem3  16112  lgsquad3  16117  m1lgs  16118  p1evtxdeqfilem  16466  peano4nninf  16954  nninfalllem1  16956  nninfall  16957  nninfsellemqall  16963  qdencn  16977  qdiff  17003