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 ⊢ (𝜑 → 𝐶 = 𝐷)

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  5799  fvmptt  5800  fsnunfv  5919  f1ocnvfv1  5986  f1ocnvfv2  5987  fcof1  5992  caov12d  6274  caov13d  6276  caov411d  6278  caovimo  6286  tfrlem5  6590  tfrlemiubacc  6606  tfr1onlemubacc  6622  tfrcllemubacc  6635  nndir  6768  en2  7118  fopwdom  7142  updjud  7428  omp1eomlem  7440  addassnqg  7755  distrnqg  7760  enq0tr  7807  distrnq0  7832  distnq0r  7836  addnqprl  7902  addnqpru  7903  appdivnq  7936  ltmprr  8015  addcmpblnr  8112  mulcmpblnrlemg  8113  ltsrprg  8120  1idsr  8141  pn0sr  8144  mulgt0sr  8151  map2psrprg  8178  axmulass  8246  ax0id  8251  recriota  8263  mul12  8462  mul4  8465  readdcan  8473  add12  8491  cnegexlem2  8509  addcan  8513  ppncan  8575  addsub4  8576  subeqxfrd  8696  subaddeqd  8702  muladd  8718  mulcanapd  8997  receuap  9007  div13ap  9031  divdivdivap  9051  divcanap5  9052  divdivap1  9061  divdivap2  9062  halfaddsub  9550  lincmble  10422  fztp  10501  fseq1p1m1  10517  flqzadd  10753  flqdiv  10778  mulp1mod1  10822  modqnegd  10836  modqsub12d  10838  q2submod  10842  modsumfzodifsn  10853  seq3m1  10930  seq3caopr  10952  seqcaoprg  10953  iseqf1olemab  10959  iseqf1olemnanb  10960  seq3f1olemqsumk  10969  seqf1og  10978  exprecap  11037  expsubap  11044  zesq  11116  nn0opthlem1d  11179  facnn2  11193  faclbnd6  11203  bcm1n  11228  hashfibclem  11303  hashfac  11309  zfz1isolemsplit  11311  seq3coll  11315  ccatopth  11509  shftval3  11613  crre  11643  resub  11656  imsub  11664  cjsub  11678  sq01  11681  bdtrilem  12029  bdtri  12030  climshft2  12096  nnf1o  12167  fsumf1o  12181  isumss  12182  fisumss  12183  fsumadd  12197  isumclim3  12214  fsummulc2  12239  fsumsub  12243  telfsumo  12257  telfsumo2  12258  hashiun  12269  bcxmas  12280  isumshft  12281  trireciplem  12291  geoserap  12298  geo2sum2  12306  fprodf1o  12379  prodssdc  12380  fprodssdc  12381  fprodmul  12382  fprodm1  12389  sinsub  12531  cossub  12532  p1modz1  12585  bitsinv1lem  12752  bitsinv1  12753  gcdaddm  12785  modgcd  12792  bezoutlemnewy  12797  absmulgcd  12818  gcdmultiplez  12822  eucalg  12861  lcmgcd  12880  lcmid  12882  numdensq  13006  dfphi2  13026  phiprm  13029  fermltl  13040  prmdiveq  13042  hashgcdlem  13044  odzdvds  13052  powm2modprm  13059  modprm0  13061  coprimeprodsq  13064  pythagtriplem6  13077  pythagtriplem7  13078  pythagtriplem12  13082  pythagtriplem14  13084  pythagtriplem16  13086  pcaddlem  13146  sumhashdc  13154  fldivp1  13155  pcfac  13157  pockthlem  13163  4sqlem12  13209  4sqlem15  13212  ennnfonelem1  13355  ennnfonelemex  13362  topnpropgd  13665  qusaddvallemg  13712  grpinvalem  13763  grpinva  13764  grprida  13765  mnd12g  13799  resmhm  13852  grprcan  13900  grplcan  13925  grpasscan1  13926  grpinv11  13932  grpinvnz  13934  grplmulf1o  13937  grpinvpropdg  13938  grpinvadd  13941  grpsubsub4  13956  dfgrp3m  13962  imasgrp2  13971  mhmid  13976  mhmmnd  13977  mulgz  14011  mulgdirlem  14014  mulgdir  14015  mulgass  14020  mulgsubdir  14023  mulgpropdg  14025  isnsg3  14068  nmzsubg  14071  ssnmz  14072  eqger  14085  eqglact  14086  ghminv  14111  conjnmz  14140  cntzsubg  14170  cntzmhm  14172  ghmcmn  14220  gzsumconst  14232  gzsummhm2  14235  gsummhm2fi  14264  rnglz  14350  rngrz  14351  isrngd  14358  ringcom  14442  crngpropd  14450  isringd  14452  ringlz  14454  ringrz  14455  ring1eq0  14459  ringmneg1  14464  mulgass3  14499  unitgrp  14531  rngidpropdg  14561  invrpropdg  14564  isrhm2d  14580  rhmunitinv  14593  subrngpropd  14632  subrginv  14653  subrgunit  14655  subrgpropd  14669  rhmpropd  14670  unitrrg  14684  aprlring  14708  lmodvs0  14767  lmodvneg1  14775  lmodcom  14778  lmodsubdi  14789  lss0v  14875  lidlrsppropdg  14940  mulgrhm2  15053  znidomb  15101  asclpropd  15148  psrass1filem  15186  psrlidmfi  15208  psrridmfi  15209  mvrf1fi  15219  mplsubgfilemcl  15232  restin  15419  blpnfctr  15682  xmssym  15712  limcimolemlt  15907  dvmulxxbr  15945  dvrecap  15956  dvmptaddx  15962  dvmptmulx  15963  dvmptnegcn  15965  dvmptsubcn  15966  dvmptcjx  15967  dveflem  15969  plymullem1  15991  dvply1  16008  sin0pilem1  16025  ptolemy  16068  tangtx  16082  rpcxpneg  16157  rpcxpsub  16158  cxprec  16160  rpcxproot  16164  cxpcom  16190  rpabscxpbnd  16192  efnthr  16193  zprmlogbaplem3  16234  pellexlem2  16247  wilthlem1  16249  sgmppw  16303  1sgmprm  16305  1sgm2ppw  16306  ppiqub  16310  perfectlem1  16316  perfectlem2  16317  bposlem6  16333  bposlem9  16336  lgsvalmod  16360  lgsneg  16365  lgsdilem  16368  lgsne0  16379  lgssq  16381  lgssq2  16382  gausslemma2dlem1f1o  16401  gausslemma2dlem6  16408  gausslemma2d  16410  lgseisenlem1  16411  lgseisenlem2  16412  lgseisenlem4  16414  lgsquadlem1  16418  lgsquadlem3  16420  lgsquad3  16425  m1lgs  16426  p1evtxdeqfilem  16774  peano4nninf  17272  nninfalllem1  17274  nninfall  17275  nninfsellemqall  17281  qdencn  17295  qdiff  17322