Theorem 3eqtr3d 1513

Description: A deduction from three chained equalities.

Hypotheses

Ref	Expression
3eqtr3d.1	⊢ (φ → A = B)
3eqtr3d.2	⊢ (φ → A = C)
3eqtr3d.3	⊢ (φ → B = D)

Assertion

Ref	Expression
3eqtr3d	⊢ (φ → C = D)

Proof of Theorem 3eqtr3d

Step	Hyp	Ref	Expression
1		3eqtr3d.2	. 2 ⊢ (φ → A = C)
2		3eqtr3d.1	. . 3 ⊢ (φ → A = B)
3		3eqtr3d.3	. . 3 ⊢ (φ → B = D)
4	2, 3	eqtrd 1505	. 2 ⊢ (φ → A = D)
5	1, 4	eqtr3d 1507	1 ⊢ (φ → C = D)

Syntax hints:   → wi 3   = wceq 955

This theorem is referenced by:  csbvarg 2018  csbnestg 2033  csbima12g 3409  csbfv12g 3737  f1ocnvfv1 3873  f1ocnvfv2 3874  csboprg 3981  mapenlem1 4478  mapenlem2 4479  phplem4 4500  php3 4504  cardiun 4842  add12t 5319  add4t 5321  cnegextlem2 5329  csbnegg 5347  addsubasst 5366  mul12t 5401  mul4t 5403  muladdt 5404  negsubdit 5440  nncant 5452  addsub4t 5456  pnncant 5463  ppncant 5464  div13t 5716  divsubdirt 5741  divcan5t 5747  divadddivt 5750  divdivdivt 5751  divdivmult 5761  halfaddsubt 5998  uzindOLD 6166  seq1m1 6269  shftval3t 6298  seqzm1 6494  sqr11 6648  reret 6749  resubt 6756  imsubt 6759  cjsubt 6766  recjt 6768  facnn2t 6891  faclbnd6 6906  sumeq2 6938  fsum1s 6962  fsump1s 6966  fsum3 6977  fsum4 6978  csbfsum 6980  fsummulc2 6987  serz1p 7005  serzsplit 7009  bcxmas 7029  geolimilem 7187  mulc1cncf 7231  efaddlem5 7301  efne0t 7328  sinsubt 7414  cossubt 7415  tgtop11t 7594  ioo2bl 7874  grpideu 8015  grprcan 8025  grpinvid1 8034  grplcan 8037  isgrp2i 8038  grpasscan1 8039  grpinvop 8042  grppnpcan2 8054  abl4 8068  ablmul 8095  ghgrpilem4 8100  ghgrpi 8101  vcsubdir 8139  vc0 8152  vcm 8154  vcoprne 8162  nvadd12 8206  nvscom 8214  nvmul0or 8236  nvz0 8260  ipid 8325  sspz 8356  lno0 8379  lnomul 8382  ipasslem3 8451  ipasslem4 8452  ipdi 8462  ipassr 8465  ipsubdi 8468  sin2pim 8646  cos2pim 8647  efper 8702  hvmul0ort 8849  hvadd12t 8859  hvadd4t 8860  hvmulcomt 8867  hvsubdistr2t 8872  normnegt 8966  chj12t 9412  h1de2b 9432  h1de2bOLD 9433  spanunsn 9459  5oalem2 9557  3oalem2 9565  mayete3 9630  hoadd4t 9667  homul12t 9688  honegnegt 9689  hosubdit 9691  honegsubdit 9693  hosub4t 9696  adj2t 9815  lnopmult 9848  lnopadd 9852  lnfnadd 9928  lnfnmul 9929  cnlnadjlem6 9961  adjlnopt 9975  adjeq0 9980  bra11 9997  leopmult 10023  hmopidmchlem 10034  pjhmopidm 10066  hstnmoct 10106  strlem1 10133  irredlem3 10275  ghomf1olem 10352  mslb1 10545  trnij 10553

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 962  ax-17 970  ax-4 972  ax-5o 974  ax-ext 1458

This theorem depends on definitions:  df-bi 147  df-an 225  df-cleq 1468

Copyright terms: Public domain