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  5607  fvmptt  5608  fsnunfv  5718  f1ocnvfv1  5778  f1ocnvfv2  5779  fcof1  5784  caov12d  6056  caov13d  6058  caov411d  6060  caovimo  6068  tfrlem5  6315  tfrlemiubacc  6331  tfr1onlemubacc  6347  tfrcllemubacc  6360  nndir  6491  fopwdom  6836  updjud  7081  omp1eomlem  7093  addassnqg  7381  distrnqg  7386  enq0tr  7433  distrnq0  7458  distnq0r  7462  addnqprl  7528  addnqpru  7529  appdivnq  7562  ltmprr  7641  addcmpblnr  7738  mulcmpblnrlemg  7739  ltsrprg  7746  1idsr  7767  pn0sr  7770  mulgt0sr  7777  map2psrprg  7804  axmulass  7872  ax0id  7877  recriota  7889  mul12  8086  mul4  8089  readdcan  8097  add12  8115  cnegexlem2  8133  addcan  8137  ppncan  8199  addsub4  8200  subeqxfrd  8320  subaddeqd  8326  muladd  8341  mulcanapd  8618  receuap  8626  div13ap  8650  divdivdivap  8670  divcanap5  8671  divdivap1  8680  divdivap2  8681  halfaddsub  9153  fztp  10078  fseq1p1m1  10094  flqzadd  10298  flqdiv  10321  mulp1mod1  10365  modqnegd  10379  modqsub12d  10381  q2submod  10385  modsumfzodifsn  10396  seq3m1  10468  seq3caopr  10483  iseqf1olemab  10489  iseqf1olemnanb  10490  seq3f1olemqsumk  10499  exprecap  10561  expsubap  10568  zesq  10639  nn0opthlem1d  10700  facnn2  10714  faclbnd6  10724  zfz1isolemsplit  10818  seq3coll  10822  shftval3  10836  crre  10866  resub  10879  imsub  10887  cjsub  10901  bdtrilem  11247  bdtri  11248  climshft2  11314  nnf1o  11384  fsumf1o  11398  isumss  11399  fisumss  11400  fsumadd  11414  isumclim3  11431  fsummulc2  11456  fsumsub  11460  telfsumo  11474  telfsumo2  11475  hashiun  11486  bcxmas  11497  isumshft  11498  trireciplem  11508  geoserap  11515  geo2sum2  11523  fprodf1o  11596  prodssdc  11597  fprodssdc  11598  fprodmul  11599  fprodm1  11606  sinsub  11748  cossub  11749  p1modz1  11801  gcdaddm  11985  modgcd  11992  bezoutlemnewy  11997  absmulgcd  12018  gcdmultiplez  12022  eucalg  12059  lcmgcd  12078  lcmid  12080  numdensq  12202  dfphi2  12220  phiprm  12223  fermltl  12234  prmdiveq  12236  hashgcdlem  12238  odzdvds  12245  powm2modprm  12252  modprm0  12254  coprimeprodsq  12257  pythagtriplem6  12270  pythagtriplem7  12271  pythagtriplem12  12275  pythagtriplem14  12277  pythagtriplem16  12279  pcaddlem  12338  sumhashdc  12345  fldivp1  12346  pcfac  12348  pockthlem  12354  ennnfonelem1  12408  ennnfonelemex  12415  topnpropgd  12702  qusaddvallemg  12752  grprinvlem  12804  grprinvd  12805  grpridd  12806  mnd12g  12829  grprcan  12910  grplcan  12932  grpasscan1  12933  grpinv11  12939  grpinvnz  12941  grplmulf1o  12944  grpinvpropdg  12945  grpinvadd  12948  grpsubsub4  12963  dfgrp3m  12969  mhmid  12979  mhmmnd  12980  mulgz  13011  mulgdirlem  13014  mulgdir  13015  mulgass  13020  mulgsubdir  13023  mulgpropdg  13025  isnsg3  13067  nmzsubg  13070  ssnmz  13071  eqger  13083  eqglact  13084  ringcom  13214  crngpropd  13218  isringd  13220  ringlz  13222  ringrz  13223  ring1eq0  13225  ringmneg1  13230  mulgass3  13254  unitgrp  13285  rngidpropdg  13315  invrpropdg  13318  subrginv  13358  subrgunit  13360  subrgpropd  13369  lmodvs0  13412  lmodvneg1  13420  lmodcom  13423  lmodsubdi  13434  restin  13679  blpnfctr  13942  xmssym  13972  limcimolemlt  14136  dvmulxxbr  14169  dvrecap  14180  dvmptaddx  14184  dvmptmulx  14185  dvmptnegcn  14187  dvmptsubcn  14188  dvmptcjx  14189  dveflem  14190  sin0pilem1  14205  ptolemy  14248  tangtx  14262  rpcxpneg  14331  rpcxpsub  14332  cxprec  14334  rpcxproot  14337  cxpcom  14360  rpabscxpbnd  14362  lgsvalmod  14423  lgsneg  14428  lgsdilem  14431  lgsne0  14442  lgssq  14444  lgssq2  14445  lgseisenlem1  14453  lgseisenlem2  14454  m1lgs  14455  peano4nninf  14758  nninfalllem1  14760  nninfall  14761  nninfsellemqall  14767  qdencn  14778