Theorem 3eqtr3g 2793

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 2784	. 2 ⊢ (𝜑 → 𝐶 = 𝐵)
4		3eqtr3g.3	. 2 ⊢ 𝐵 = 𝐷
5	3, 4	eqtrdi 2786	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 2007  ax-9 2118  ax-ext 2707

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

This theorem is referenced by:  csbnest1g  4407  disjdif2  4455  diftpsn3  4778  tppreqb  4781  xpid11  5912  cores2  6248  funcoeqres  6848  fvunsn  7170  caovmo  7642  dftpos2  8240  fvmpocurryd  8268  tfrlem16  8405  oev2  8533  domss2  9148  enp1ilem  9282  fipreima  9368  dfac5lem3  10137  fpwwe2lem12  10654  canthwelem  10662  canthp1lem2  10665  reclem3pr  11061  mulcmpblnrlem  11082  1idsr  11110  mulgt0sr  11117  mul02lem2  11410  ine0  11670  lo1eq  15582  rlimeq  15583  sumeq2ii  15707  fsumf1o  15737  sumss  15738  fsumss  15739  fsumadd  15754  fsumcom2  15788  fsum0diag2  15797  fsummulc2  15798  fsumrelem  15821  isumshft  15853  mertenslem1  15898  prodeq2ii  15925  fprodf1o  15960  prodss  15961  fprodss  15962  fprodmul  15974  fproddiv  15975  fprodcom2  15998  fprodmodd  16011  fprodefsum  16109  bitsinv1  16459  bitsinvp1  16466  4sqlem10  16965  setsnid  17225  topnpropd  17448  xpsff1o  17579  homfeqbas  17706  comfffval2  17711  comfeq  17716  oppchomfpropd  17736  isssc  17831  funcpropd  17913  hofpropd  18277  eqglact  19160  symgvalstruct  19376  lsmmod2  19655  vrgpinv  19748  frgpnabllem1  19852  frgpnabllem2  19853  gsum2dlem2  19950  dprddisj2  20020  ablfac1eulem  20053  ringpropd  20246  crngpropd  20247  mulgass3  20311  rngidpropd  20373  invrpropd  20376  isrhm2d  20445  subrngpropd  20526  subrgpropd  20566  rhmpropd  20567  lss0v  20972  lidlrsppropd  21203  ressmpladd  21985  ressmplmul  21986  ressmplvsca  21987  eqcoe1ply1eq  22235  resstopn  23122  lecldbas  23155  isref  23445  txhaus  23583  qustgplem  24057  tuslem  24203  imasdsf1olem  24310  metustsym  24492  reconnlem1  24764  voliunlem1  25501  ismbf3d  25605  i1fima  25629  i1fd  25632  itgfsum  25778  dvmptc  25912  dvmptfsum  25929  dvfsumle  25976  dvfsumleOLD  25977  dvfsumlem2  25983  dvfsumlem2OLD  25984  itgsubst  26006  atantayl2  26898  chtdif  27118  ppidif  27123  fsumdvdsmul  27155  sltonold  28200  pythi  30777  hvsubeq0i  30990  hvaddcani  30992  cmcmlem  31518  pj11i  31638  hosubeq0i  31753  riesz3i  31989  pjclem1  32122  pjclem3  32124  st0  32176  chirredi  32321  mdsymi  32338  difeq  32445  unidifsnne  32463  1nei  32660  subrgchr  33178  ressply1evls1  33524  locfinref  33818  esumpfinvallem  34051  esum2dlem  34069  carsgclctun  34299  ballotlemgun  34503  cvmliftmolem1  35249  cvmlift3lem6  35292  msubff1  35524  isfne  36303  isfne4  36304  isfne4b  36305  bj-1uplth  36971  bj-2uplth  36985  matunitlindflem1  37586  ptrest  37589  poimirlem3  37593  poimirlem4  37594  poimirlem8  37598  poimirlem15  37605  mblfinlem2  37628  voliunnfl  37634  cdlemg47  40701  ltrnco4  40704  sn-1ne2  42262  sn-0tie0  42429  sn-inelr  42457  eldioph2  42732  binomcxplemdvbinom  44325  binomcxplemnotnn0  44328  compne  44413  rnfdmpr  47258  cycl3grtri  47907