Theorem 3eqtr3g 2787

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

Syntax hints:   → wi 4   = wceq 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721

This theorem is referenced by:  csbnest1g  4391  disjdif2  4439  diftpsn3  4762  tppreqb  4765  xpid11  5885  cores2  6220  funcoeqres  6813  fvunsn  7135  caovmo  7606  dftpos2  8199  fvmpocurryd  8227  tfrlem16  8338  oev2  8464  domss2  9077  enp1ilem  9199  fipreima  9285  dfac5lem3  10054  fpwwe2lem12  10571  canthwelem  10579  canthp1lem2  10582  reclem3pr  10978  mulcmpblnrlem  10999  1idsr  11027  mulgt0sr  11034  mul02lem2  11327  ine0  11589  lo1eq  15510  rlimeq  15511  sumeq2ii  15635  fsumf1o  15665  sumss  15666  fsumss  15667  fsumadd  15682  fsumcom2  15716  fsum0diag2  15725  fsummulc2  15726  fsumrelem  15749  isumshft  15781  mertenslem1  15826  prodeq2ii  15853  fprodf1o  15888  prodss  15889  fprodss  15890  fprodmul  15902  fproddiv  15903  fprodcom2  15926  fprodmodd  15939  fprodefsum  16037  bitsinv1  16388  bitsinvp1  16395  4sqlem10  16894  setsnid  17154  topnpropd  17375  xpsff1o  17506  homfeqbas  17637  comfffval2  17642  comfeq  17647  oppchomfpropd  17667  isssc  17762  funcpropd  17844  hofpropd  18208  eqglact  19093  symgvalstruct  19311  lsmmod2  19590  vrgpinv  19683  frgpnabllem1  19787  frgpnabllem2  19788  gsum2dlem2  19885  dprddisj2  19955  ablfac1eulem  19988  ringpropd  20208  crngpropd  20209  mulgass3  20273  rngidpropd  20335  invrpropd  20338  isrhm2d  20407  subrngpropd  20488  subrgpropd  20528  rhmpropd  20529  lss0v  20955  lidlrsppropd  21186  ressmpladd  21969  ressmplmul  21970  ressmplvsca  21971  eqcoe1ply1eq  22219  resstopn  23106  lecldbas  23139  isref  23429  txhaus  23567  qustgplem  24041  tuslem  24187  imasdsf1olem  24294  metustsym  24476  reconnlem1  24748  voliunlem1  25484  ismbf3d  25588  i1fima  25612  i1fd  25615  itgfsum  25761  dvmptc  25895  dvmptfsum  25912  dvfsumle  25959  dvfsumleOLD  25960  dvfsumlem2  25966  dvfsumlem2OLD  25967  itgsubst  25989  atantayl2  26881  chtdif  27101  ppidif  27106  fsumdvdsmul  27138  onsleft  28201  onscutlt  28205  pythi  30829  hvsubeq0i  31042  hvaddcani  31044  cmcmlem  31570  pj11i  31690  hosubeq0i  31805  riesz3i  32041  pjclem1  32174  pjclem3  32176  st0  32228  chirredi  32373  mdsymi  32390  difeq  32497  unidifsnne  32515  1nei  32710  subrgchr  33204  ressply1evls1  33527  locfinref  33824  esumpfinvallem  34057  esum2dlem  34075  carsgclctun  34305  ballotlemgun  34509  cvmliftmolem1  35261  cvmlift3lem6  35304  msubff1  35536  isfne  36320  isfne4  36321  isfne4b  36322  bj-1uplth  36988  bj-2uplth  37002  matunitlindflem1  37603  ptrest  37606  poimirlem3  37610  poimirlem4  37611  poimirlem8  37615  poimirlem15  37622  mblfinlem2  37645  voliunnfl  37651  cdlemg47  40723  ltrnco4  40726  sn-1ne2  42246  sn-00idlem3  42381  sn-0tie0  42432  sn-inelr  42468  eldioph2  42743  binomcxplemdvbinom  44335  binomcxplemnotnn0  44338  compne  44423  rnfdmpr  47275  cycl3grtri  47939