Theorem 3eqtr3g 2799

Description: A chained equality inference, useful for converting from definitions. (Contributed by NM, 15-Nov-1994.)

Hypotheses

Ref	Expression
3eqtr3g.1	⊢ (𝜑 → 𝐴 = 𝐵)
3eqtr3g.2	⊢ 𝐴 = 𝐶
3eqtr3g.3	⊢ 𝐵 = 𝐷

Assertion

Ref	Expression
3eqtr3g	⊢ (𝜑 → 𝐶 = 𝐷)

Proof of Theorem 3eqtr3g

Step	Hyp	Ref	Expression
1		3eqtr3g.2	. . 3 ⊢ 𝐴 = 𝐶
2		3eqtr3g.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
3	1, 2	eqtr3id 2790	. 2 ⊢ (𝜑 → 𝐶 = 𝐵)
4		3eqtr3g.3	. 2 ⊢ 𝐵 = 𝐷
5	3, 4	eqtrdi 2792	1 ⊢ (𝜑 → 𝐶 = 𝐷)

Syntax hints:   → wi 4   = wceq 1548

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-ex 1788  df-cleq 2733

This theorem is referenced by:  csbnest1g  4363  disjdif2  4411  diftpsn3  4738  tppreqb  4741  xpid11  5881  cores2  6215  funcoeqres  6802  fvunsn  7127  caovmo  7597  dftpos2  8187  fvmpocurryd  8215  tfrlem16  8326  oev2  8452  domss2  9068  enp1ilem  9182  fipreima  9262  dfac5lem3  10042  fpwwe2lem12  10560  canthwelem  10568  canthp1lem2  10571  reclem3pr  10967  mulcmpblnrlem  10988  1idsr  11016  mulgt0sr  11023  mul02lem2  11318  ine0  11580  lo1eq  15525  rlimeq  15526  sumeq2ii  15650  fsumf1o  15680  sumss  15681  fsumss  15682  fsumadd  15697  fsumcom2  15731  fsum0diag2  15740  fsummulc2  15741  fsumrelem  15765  isumshft  15799  mertenslem1  15844  prodeq2ii  15871  fprodf1o  15906  prodss  15907  fprodss  15908  fprodmul  15920  fproddiv  15921  fprodcom2  15944  fprodmodd  15957  fprodefsum  16055  bitsinv1  16406  bitsinvp1  16413  4sqlem10  16913  setsnid  17173  topnpropd  17394  xpsff1o  17526  homfeqbas  17657  comfffval2  17662  comfeq  17667  oppchomfpropd  17687  isssc  17782  funcpropd  17864  hofpropd  18228  eqglact  19149  symgvalstruct  19367  lsmmod2  19646  vrgpinv  19739  frgpnabllem1  19843  frgpnabllem2  19844  gsum2dlem2  19941  dprddisj2  20011  ablfac1eulem  20044  ringpropd  20264  crngpropd  20265  mulgass3  20328  rngidpropd  20390  invrpropd  20393  isrhm2d  20462  subrngpropd  20544  subrgpropd  20584  rhmpropd  20585  lss0v  21010  lidlrsppropd  21241  ressmpladd  22008  ressmplmul  22009  ressmplvsca  22010  eqcoe1ply1eq  22289  resstopn  23173  lecldbas  23206  isref  23496  txhaus  23634  qustgplem  24108  tuslem  24253  imasdsf1olem  24360  metustsym  24542  reconnlem1  24814  voliunlem1  25539  ismbf3d  25643  i1fima  25667  i1fd  25670  itgfsum  25816  dvmptc  25947  dvmptfsum  25964  dvfsumle  26010  dvfsumlem2  26016  itgsubst  26038  atantayl2  26924  chtdif  27143  ppidif  27148  fsumdvdsmul  27180  onleft  28274  oncutlt  28278  pythi  30943  hvsubeq0i  31156  hvaddcani  31158  cmcmlem  31684  pj11i  31804  hosubeq0i  31919  riesz3i  32155  pjclem1  32288  pjclem3  32290  st0  32342  chirredi  32487  mdsymi  32504  difeq  32610  unidifsnne  32628  1nei  32833  subrgchr  33322  ressply1evls1  33660  srapwov  33785  locfinref  34037  esumpfinvallem  34270  esum2dlem  34288  carsgclctun  34517  ballotlemgun  34721  cvmliftmolem1  35524  cvmlift3lem6  35567  msubff1  35799  isfne  36582  isfne4  36583  isfne4b  36584  bj-1uplth  37375  bj-2uplth  37389  matunitlindflem1  37998  ptrest  38001  poimirlem3  38005  poimirlem4  38006  poimirlem8  38010  poimirlem15  38017  mblfinlem2  38040  voliunnfl  38046  cdlemg47  41243  ltrnco4  41246  sn-1ne2  42763  sn-00idlem3  42892  sn-0tie0  42956  sn-inelr  42992  eldioph2  43226  binomcxplemdvbinom  44812  binomcxplemnotnn0  44815  compne  44899  rnfdmpr  47758  cycl3grtri  48452