Theorem 3eqtr3d 2270

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

Syntax hints:   → wi 4   = wceq 1395

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 1493  ax-gen 1495  ax-4 1556  ax-17 1572  ax-ext 2211

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

This theorem is referenced by:  mpteqb  5727  fvmptt  5728  fsnunfv  5844  f1ocnvfv1  5907  f1ocnvfv2  5908  fcof1  5913  caov12d  6193  caov13d  6195  caov411d  6197  caovimo  6205  tfrlem5  6466  tfrlemiubacc  6482  tfr1onlemubacc  6498  tfrcllemubacc  6511  nndir  6644  en2  6981  fopwdom  7005  updjud  7260  omp1eomlem  7272  addassnqg  7580  distrnqg  7585  enq0tr  7632  distrnq0  7657  distnq0r  7661  addnqprl  7727  addnqpru  7728  appdivnq  7761  ltmprr  7840  addcmpblnr  7937  mulcmpblnrlemg  7938  ltsrprg  7945  1idsr  7966  pn0sr  7969  mulgt0sr  7976  map2psrprg  8003  axmulass  8071  ax0id  8076  recriota  8088  mul12  8286  mul4  8289  readdcan  8297  add12  8315  cnegexlem2  8333  addcan  8337  ppncan  8399  addsub4  8400  subeqxfrd  8520  subaddeqd  8526  muladd  8541  mulcanapd  8819  receuap  8827  div13ap  8851  divdivdivap  8871  divcanap5  8872  divdivap1  8881  divdivap2  8882  halfaddsub  9356  fztp  10286  fseq1p1m1  10302  flqzadd  10530  flqdiv  10555  mulp1mod1  10599  modqnegd  10613  modqsub12d  10615  q2submod  10619  modsumfzodifsn  10630  seq3m1  10707  seq3caopr  10729  seqcaoprg  10730  iseqf1olemab  10736  iseqf1olemnanb  10737  seq3f1olemqsumk  10746  seqf1og  10755  exprecap  10814  expsubap  10821  zesq  10892  nn0opthlem1d  10954  facnn2  10968  faclbnd6  10978  zfz1isolemsplit  11073  seq3coll  11077  ccatopth  11263  shftval3  11353  crre  11383  resub  11396  imsub  11404  cjsub  11418  bdtrilem  11765  bdtri  11766  climshft2  11832  nnf1o  11902  fsumf1o  11916  isumss  11917  fisumss  11918  fsumadd  11932  isumclim3  11949  fsummulc2  11974  fsumsub  11978  telfsumo  11992  telfsumo2  11993  hashiun  12004  bcxmas  12015  isumshft  12016  trireciplem  12026  geoserap  12033  geo2sum2  12041  fprodf1o  12114  prodssdc  12115  fprodssdc  12116  fprodmul  12117  fprodm1  12124  sinsub  12266  cossub  12267  p1modz1  12320  bitsinv1lem  12487  bitsinv1  12488  gcdaddm  12520  modgcd  12527  bezoutlemnewy  12532  absmulgcd  12553  gcdmultiplez  12557  eucalg  12596  lcmgcd  12615  lcmid  12617  numdensq  12739  dfphi2  12757  phiprm  12760  fermltl  12771  prmdiveq  12773  hashgcdlem  12775  odzdvds  12783  powm2modprm  12790  modprm0  12792  coprimeprodsq  12795  pythagtriplem6  12808  pythagtriplem7  12809  pythagtriplem12  12813  pythagtriplem14  12815  pythagtriplem16  12817  pcaddlem  12877  sumhashdc  12885  fldivp1  12886  pcfac  12888  pockthlem  12894  4sqlem12  12940  4sqlem15  12943  ennnfonelem1  12993  ennnfonelemex  13000  topnpropgd  13301  qusaddvallemg  13381  grpinvalem  13433  grpinva  13434  grprida  13435  mnd12g  13476  resmhm  13535  grprcan  13585  grplcan  13610  grpasscan1  13611  grpinv11  13617  grpinvnz  13619  grplmulf1o  13622  grpinvpropdg  13623  grpinvadd  13626  grpsubsub4  13641  dfgrp3m  13647  imasgrp2  13662  mhmid  13667  mhmmnd  13668  mulgz  13702  mulgdirlem  13705  mulgdir  13706  mulgass  13711  mulgsubdir  13714  mulgpropdg  13716  isnsg3  13759  nmzsubg  13762  ssnmz  13763  eqger  13776  eqglact  13777  ghminv  13802  conjnmz  13831  ghmcmn  13879  gsumfzconst  13893  gsumfzmhm2  13896  rnglz  13923  rngrz  13924  isrngd  13931  ringcom  14009  crngpropd  14017  isringd  14019  ringlz  14021  ringrz  14022  ring1eq0  14026  ringmneg1  14031  mulgass3  14063  unitgrp  14095  rngidpropdg  14125  invrpropdg  14128  isrhm2d  14144  rhmunitinv  14157  subrngpropd  14195  subrginv  14216  subrgunit  14218  subrgpropd  14232  rhmpropd  14233  unitrrg  14246  lmodvs0  14301  lmodvneg1  14309  lmodcom  14312  lmodsubdi  14323  lss0v  14409  lidlrsppropdg  14474  mulgrhm2  14589  znidomb  14637  restin  14865  blpnfctr  15128  xmssym  15158  limcimolemlt  15353  dvmulxxbr  15391  dvrecap  15402  dvmptaddx  15408  dvmptmulx  15409  dvmptnegcn  15411  dvmptsubcn  15412  dvmptcjx  15413  dveflem  15415  plymullem1  15437  dvply1  15454  sin0pilem1  15470  ptolemy  15513  tangtx  15527  rpcxpneg  15596  rpcxpsub  15597  cxprec  15599  rpcxproot  15603  cxpcom  15627  rpabscxpbnd  15629  wilthlem1  15669  sgmppw  15681  1sgmprm  15683  1sgm2ppw  15684  perfectlem1  15688  perfectlem2  15689  lgsvalmod  15713  lgsneg  15718  lgsdilem  15721  lgsne0  15732  lgssq  15734  lgssq2  15735  gausslemma2dlem1f1o  15754  gausslemma2dlem6  15761  gausslemma2d  15763  lgseisenlem1  15764  lgseisenlem2  15765  lgseisenlem4  15767  lgsquadlem1  15771  lgsquadlem3  15773  lgsquad3  15778  m1lgs  15779  peano4nninf  16432  nninfalllem1  16434  nninfall  16435  nninfsellemqall  16441  qdencn  16455