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  10056  fpwwe2lem12  10573  canthwelem  10581  canthp1lem2  10584  reclem3pr  10980  mulcmpblnrlem  11001  1idsr  11029  mulgt0sr  11036  mul02lem2  11329  ine0  11591  lo1eq  15511  rlimeq  15512  sumeq2ii  15636  fsumf1o  15666  sumss  15667  fsumss  15668  fsumadd  15683  fsumcom2  15717  fsum0diag2  15726  fsummulc2  15727  fsumrelem  15750  isumshft  15782  mertenslem1  15827  prodeq2ii  15854  fprodf1o  15889  prodss  15890  fprodss  15891  fprodmul  15903  fproddiv  15904  fprodcom2  15927  fprodmodd  15940  fprodefsum  16038  bitsinv1  16389  bitsinvp1  16396  4sqlem10  16895  setsnid  17155  topnpropd  17376  xpsff1o  17507  homfeqbas  17638  comfffval2  17643  comfeq  17648  oppchomfpropd  17668  isssc  17763  funcpropd  17845  hofpropd  18209  eqglact  19094  symgvalstruct  19312  lsmmod2  19591  vrgpinv  19684  frgpnabllem1  19788  frgpnabllem2  19789  gsum2dlem2  19886  dprddisj2  19956  ablfac1eulem  19989  ringpropd  20209  crngpropd  20210  mulgass3  20274  rngidpropd  20336  invrpropd  20339  isrhm2d  20408  subrngpropd  20489  subrgpropd  20529  rhmpropd  20530  lss0v  20956  lidlrsppropd  21187  ressmpladd  21970  ressmplmul  21971  ressmplvsca  21972  eqcoe1ply1eq  22220  resstopn  23107  lecldbas  23140  isref  23430  txhaus  23568  qustgplem  24042  tuslem  24188  imasdsf1olem  24295  metustsym  24477  reconnlem1  24749  voliunlem1  25485  ismbf3d  25589  i1fima  25613  i1fd  25616  itgfsum  25762  dvmptc  25896  dvmptfsum  25913  dvfsumle  25960  dvfsumleOLD  25961  dvfsumlem2  25967  dvfsumlem2OLD  25968  itgsubst  25990  atantayl2  26882  chtdif  27102  ppidif  27107  fsumdvdsmul  27139  onsleft  28202  onscutlt  28206  pythi  30830  hvsubeq0i  31043  hvaddcani  31045  cmcmlem  31571  pj11i  31691  hosubeq0i  31806  riesz3i  32042  pjclem1  32175  pjclem3  32177  st0  32229  chirredi  32374  mdsymi  32391  difeq  32498  unidifsnne  32516  1nei  32711  subrgchr  33205  ressply1evls1  33528  locfinref  33825  esumpfinvallem  34058  esum2dlem  34076  carsgclctun  34306  ballotlemgun  34510  cvmliftmolem1  35262  cvmlift3lem6  35305  msubff1  35537  isfne  36321  isfne4  36322  isfne4b  36323  bj-1uplth  36989  bj-2uplth  37003  matunitlindflem1  37604  ptrest  37607  poimirlem3  37611  poimirlem4  37612  poimirlem8  37616  poimirlem15  37623  mblfinlem2  37646  voliunnfl  37652  cdlemg47  40724  ltrnco4  40727  sn-1ne2  42247  sn-00idlem3  42382  sn-0tie0  42433  sn-inelr  42469  eldioph2  42744  binomcxplemdvbinom  44336  binomcxplemnotnn0  44339  compne  44424  rnfdmpr  47276  cycl3grtri  47940