Theorem 3eqtr3d 2155

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

Syntax hints:   → wi 4   = wceq 1314

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1406  ax-gen 1408  ax-4 1470  ax-17 1489  ax-ext 2097

This theorem depends on definitions:  df-bi 116  df-cleq 2108

This theorem is referenced by:  mpteqb  5465  fvmptt  5466  fsnunfv  5575  f1ocnvfv1  5632  f1ocnvfv2  5633  fcof1  5638  caov12d  5906  caov13d  5908  caov411d  5910  caovimo  5918  grprinvlem  5919  grprinvd  5920  grpridd  5921  tfrlem5  6165  tfrlemiubacc  6181  tfr1onlemubacc  6197  tfrcllemubacc  6210  nndir  6340  fopwdom  6683  updjud  6919  omp1eomlem  6931  addassnqg  7138  distrnqg  7143  enq0tr  7190  distrnq0  7215  distnq0r  7219  addnqprl  7285  addnqpru  7286  appdivnq  7319  ltmprr  7398  addcmpblnr  7482  mulcmpblnrlemg  7483  ltsrprg  7490  1idsr  7511  pn0sr  7514  mulgt0sr  7520  axmulass  7608  ax0id  7613  recriota  7625  mul12  7814  mul4  7817  readdcan  7825  add12  7843  cnegexlem2  7861  addcan  7865  ppncan  7927  addsub4  7928  subaddeqd  8050  muladd  8065  mulcanapd  8335  receuap  8343  div13ap  8366  divdivdivap  8386  divcanap5  8387  divdivap1  8396  divdivap2  8397  halfaddsub  8858  fztp  9751  fseq1p1m1  9767  flqzadd  9964  flqdiv  9987  mulp1mod1  10031  modqnegd  10045  modqsub12d  10047  q2submod  10051  modsumfzodifsn  10062  seq3m1  10134  seq3caopr  10149  iseqf1olemab  10155  iseqf1olemnanb  10156  seq3f1olemqsumk  10165  exprecap  10227  expsubap  10234  zesq  10303  nn0opthlem1d  10359  facnn2  10373  faclbnd6  10383  zfz1isolemsplit  10474  seq3coll  10478  shftval3  10492  crre  10522  resub  10535  imsub  10543  cjsub  10557  bdtrilem  10902  bdtri  10903  climshft2  10967  isummolemnm  11040  fsumf1o  11051  isumss  11052  fisumss  11053  fsumadd  11067  isumclim3  11084  fsummulc2  11109  fsumsub  11113  telfsumo  11127  telfsumo2  11128  hashiun  11139  bcxmas  11150  isumshft  11151  trireciplem  11161  geoserap  11168  geo2sum2  11176  sinsub  11298  cossub  11299  gcdaddm  11520  modgcd  11527  bezoutlemnewy  11530  absmulgcd  11551  gcdmultiplez  11555  eucalg  11586  lcmgcd  11605  lcmid  11607  numdensq  11725  dfphi2  11741  phiprm  11744  hashgcdlem  11748  ennnfonelem1  11765  ennnfonelemex  11772  topnpropgd  11977  restin  12188  blpnfctr  12428  xmssym  12458  limcimolemlt  12589  dvmulxxbr  12621  peano4nninf  12892  nninfalllem1  12895  nninfall  12896  nninfsellemqall  12903  qdencn  12914