Theorem 3eqtr3d 2237

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

Syntax hints:   → wi 4   = wceq 1364

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 1461  ax-gen 1463  ax-4 1524  ax-17 1540  ax-ext 2178

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

This theorem is referenced by:  mpteqb  5655  fvmptt  5656  fsnunfv  5766  f1ocnvfv1  5827  f1ocnvfv2  5828  fcof1  5833  caov12d  6109  caov13d  6111  caov411d  6113  caovimo  6121  tfrlem5  6381  tfrlemiubacc  6397  tfr1onlemubacc  6413  tfrcllemubacc  6426  nndir  6557  fopwdom  6906  updjud  7157  omp1eomlem  7169  addassnqg  7468  distrnqg  7473  enq0tr  7520  distrnq0  7545  distnq0r  7549  addnqprl  7615  addnqpru  7616  appdivnq  7649  ltmprr  7728  addcmpblnr  7825  mulcmpblnrlemg  7826  ltsrprg  7833  1idsr  7854  pn0sr  7857  mulgt0sr  7864  map2psrprg  7891  axmulass  7959  ax0id  7964  recriota  7976  mul12  8174  mul4  8177  readdcan  8185  add12  8203  cnegexlem2  8221  addcan  8225  ppncan  8287  addsub4  8288  subeqxfrd  8408  subaddeqd  8414  muladd  8429  mulcanapd  8707  receuap  8715  div13ap  8739  divdivdivap  8759  divcanap5  8760  divdivap1  8769  divdivap2  8770  halfaddsub  9244  fztp  10172  fseq1p1m1  10188  flqzadd  10407  flqdiv  10432  mulp1mod1  10476  modqnegd  10490  modqsub12d  10492  q2submod  10496  modsumfzodifsn  10507  seq3m1  10584  seq3caopr  10606  seqcaoprg  10607  iseqf1olemab  10613  iseqf1olemnanb  10614  seq3f1olemqsumk  10623  seqf1og  10632  exprecap  10691  expsubap  10698  zesq  10769  nn0opthlem1d  10831  facnn2  10845  faclbnd6  10855  zfz1isolemsplit  10949  seq3coll  10953  shftval3  11011  crre  11041  resub  11054  imsub  11062  cjsub  11076  bdtrilem  11423  bdtri  11424  climshft2  11490  nnf1o  11560  fsumf1o  11574  isumss  11575  fisumss  11576  fsumadd  11590  isumclim3  11607  fsummulc2  11632  fsumsub  11636  telfsumo  11650  telfsumo2  11651  hashiun  11662  bcxmas  11673  isumshft  11674  trireciplem  11684  geoserap  11691  geo2sum2  11699  fprodf1o  11772  prodssdc  11773  fprodssdc  11774  fprodmul  11775  fprodm1  11782  sinsub  11924  cossub  11925  p1modz1  11978  bitsinv1lem  12145  bitsinv1  12146  gcdaddm  12178  modgcd  12185  bezoutlemnewy  12190  absmulgcd  12211  gcdmultiplez  12215  eucalg  12254  lcmgcd  12273  lcmid  12275  numdensq  12397  dfphi2  12415  phiprm  12418  fermltl  12429  prmdiveq  12431  hashgcdlem  12433  odzdvds  12441  powm2modprm  12448  modprm0  12450  coprimeprodsq  12453  pythagtriplem6  12466  pythagtriplem7  12467  pythagtriplem12  12471  pythagtriplem14  12473  pythagtriplem16  12475  pcaddlem  12535  sumhashdc  12543  fldivp1  12544  pcfac  12546  pockthlem  12552  4sqlem12  12598  4sqlem15  12601  ennnfonelem1  12651  ennnfonelemex  12658  topnpropgd  12957  qusaddvallemg  13037  grpinvalem  13089  grpinva  13090  grprida  13091  mnd12g  13132  resmhm  13191  grprcan  13241  grplcan  13266  grpasscan1  13267  grpinv11  13273  grpinvnz  13275  grplmulf1o  13278  grpinvpropdg  13279  grpinvadd  13282  grpsubsub4  13297  dfgrp3m  13303  imasgrp2  13318  mhmid  13323  mhmmnd  13324  mulgz  13358  mulgdirlem  13361  mulgdir  13362  mulgass  13367  mulgsubdir  13370  mulgpropdg  13372  isnsg3  13415  nmzsubg  13418  ssnmz  13419  eqger  13432  eqglact  13433  ghminv  13458  conjnmz  13487  ghmcmn  13535  gsumfzconst  13549  gsumfzmhm2  13552  rnglz  13579  rngrz  13580  isrngd  13587  ringcom  13665  crngpropd  13673  isringd  13675  ringlz  13677  ringrz  13678  ring1eq0  13682  ringmneg1  13687  mulgass3  13719  unitgrp  13750  rngidpropdg  13780  invrpropdg  13783  isrhm2d  13799  rhmunitinv  13812  subrngpropd  13850  subrginv  13871  subrgunit  13873  subrgpropd  13887  rhmpropd  13888  unitrrg  13901  lmodvs0  13956  lmodvneg1  13964  lmodcom  13967  lmodsubdi  13978  lss0v  14064  lidlrsppropdg  14129  mulgrhm2  14244  znidomb  14292  restin  14520  blpnfctr  14783  xmssym  14813  limcimolemlt  15008  dvmulxxbr  15046  dvrecap  15057  dvmptaddx  15063  dvmptmulx  15064  dvmptnegcn  15066  dvmptsubcn  15067  dvmptcjx  15068  dveflem  15070  plymullem1  15092  dvply1  15109  sin0pilem1  15125  ptolemy  15168  tangtx  15182  rpcxpneg  15251  rpcxpsub  15252  cxprec  15254  rpcxproot  15258  cxpcom  15282  rpabscxpbnd  15284  wilthlem1  15324  sgmppw  15336  1sgmprm  15338  1sgm2ppw  15339  perfectlem1  15343  perfectlem2  15344  lgsvalmod  15368  lgsneg  15373  lgsdilem  15376  lgsne0  15387  lgssq  15389  lgssq2  15390  gausslemma2dlem1f1o  15409  gausslemma2dlem6  15416  gausslemma2d  15418  lgseisenlem1  15419  lgseisenlem2  15420  lgseisenlem4  15422  lgsquadlem1  15426  lgsquadlem3  15428  lgsquad3  15433  m1lgs  15434  peano4nninf  15761  nninfalllem1  15763  nninfall  15764  nninfsellemqall  15770  qdencn  15784