Theorem 3eqtr3g 2795

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

Syntax hints:   → wi 4   = wceq 1542

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729

This theorem is referenced by:  csbnest1g  4373  disjdif2  4421  diftpsn3  4746  tppreqb  4749  xpid11  5883  cores2  6220  funcoeqres  6807  fvunsn  7129  caovmo  7599  dftpos2  8188  fvmpocurryd  8216  tfrlem16  8327  oev2  8453  domss2  9069  enp1ilem  9183  fipreima  9263  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  20461  subrngpropd  20540  subrgpropd  20580  rhmpropd  20581  lss0v  21007  lidlrsppropd  21238  ressmpladd  22021  ressmplmul  22022  ressmplvsca  22023  eqcoe1ply1eq  22278  resstopn  23165  lecldbas  23198  isref  23488  txhaus  23626  qustgplem  24100  tuslem  24245  imasdsf1olem  24352  metustsym  24534  reconnlem1  24806  voliunlem1  25531  ismbf3d  25635  i1fima  25659  i1fd  25662  itgfsum  25808  dvmptc  25939  dvmptfsum  25956  dvfsumle  26002  dvfsumlem2  26008  itgsubst  26030  atantayl2  26919  chtdif  27139  ppidif  27144  fsumdvdsmul  27176  onleft  28270  oncutlt  28274  pythi  30940  hvsubeq0i  31153  hvaddcani  31155  cmcmlem  31681  pj11i  31801  hosubeq0i  31916  riesz3i  32152  pjclem1  32285  pjclem3  32287  st0  32339  chirredi  32484  mdsymi  32501  difeq  32607  unidifsnne  32625  1nei  32829  subrgchr  33317  ressply1evls1  33644  srapwov  33752  locfinref  34005  esumpfinvallem  34238  esum2dlem  34256  carsgclctun  34485  ballotlemgun  34689  cvmliftmolem1  35483  cvmlift3lem6  35526  msubff1  35758  isfne  36541  isfne4  36542  isfne4b  36543  bj-1uplth  37334  bj-2uplth  37348  matunitlindflem1  37957  ptrest  37960  poimirlem3  37964  poimirlem4  37965  poimirlem8  37969  poimirlem15  37976  mblfinlem2  37999  voliunnfl  38005  cdlemg47  41202  ltrnco4  41205  sn-1ne2  42723  sn-00idlem3  42852  sn-0tie0  42916  sn-inelr  42952  eldioph2  43214  binomcxplemdvbinom  44804  binomcxplemnotnn0  44807  compne  44891  rnfdmpr  47747  cycl3grtri  48441