Theorem 3eqtrd 1554

Description: A deduction from three chained equalities.

Hypotheses

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

Assertion

Ref	Expression
3eqtrd	⊢ (φ → A = D)

Proof of Theorem 3eqtrd

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

Syntax hints:   → wi 3   = wceq 992

This theorem is referenced by:  csbnestg 2088  csbopabg 2752  csbima12g 3505  resiima 3511  csbfv12g 3853  csboprg 4044  fparlem3 4201  fparlem4 4202  fpar 4203  onopriun 4211  om1 4312  oe1 4314  oarec 4332  nneob 4395  ac6sfilem2 4589  ltexpq 5234  halfpq 5236  addsub 5538  muladd 5575  negsubdi2 5612  nnncan1 5621  mulsub 5631  recextlem1 5838  muleqadd 5852  div23 5888  div12 5890  divdivdiv 5924  conjmul 5937  nndivtr 6106  uzindOLD 6379  fldiv 6456  modid 6471  modcyc 6475  uzrdgsuci 6668  seqz1 6742  seqzp1 6743  seq0p1 6746  seqzval2 6748  mulexp 6788  expdiv 6796  imre 6974  cjreim 7029  cjreim2 7030  cjdivi 7091  ser1absdiflem 7132  facp1 7139  bcn0 7166  bcnp11 7168  fsum1i 7208  fsump1i 7209  fsumshft 7234  fsumconst 7241  binomlem1 7269  binomlem2 7270  binomlem6 7274  isumnul 7407  arisumilem 7429  geoisumr 7448  efcltlem1 7509  ef0lem 7515  efaddlem5 7547  ef01tllem1 7588  abspef01tlubi 7603  efi4p 7643  resin4p 7644  recos4p 7645  efmival 7656  efeul 7657  absefi 7691  absefib 7693  efieq1re 7694  demoivre 7695  cnconst 7990  grpidinvlem1 8261  grpinvid2 8290  grpasscan2 8295  grpinvop 8298  grpinvdiv 8302  grppncan 8308  grpnpcan 8309  grppnpcan2 8310  gxval 8314  gxcom 8325  gxmul 8334  gxmodid 8335  ablmuldiv 8348  ablnncan 8353  gxdi 8355  ablmul 8372  ghsubgi 8379  vcz 8436  vcnegsubdi2 8441  vcoprne 8445  nvnegneg 8518  nvsubadd 8522  nvpncan2 8523  nvnncan 8530  nvdif 8540  nvpi 8541  nvabs 8548  nvge0 8549  nv1 8551  nvnd 8566  imsmetlem 8570  ipid 8617  ipcj 8621  lnocoi 8672  cnph 8734  ipasslem5 8750  ipasslem11 8756  ajval 8778  ubthlem10 8796  minveclem28 8832  spwpr4 8925  spwpr4OLD 8926  spwpr4aOLD 8927  sincolem 8932  sinper 8957  cosper 8958  sinmpi 8961  cosmpi 8962  sinppi 8963  cosppi 8964  sinhalfpip 8966  sinhalfpim 8967  coshalfpim 8969  abssinper 8980  sineq0 8983  shftefif1olem 9013  effoi 9017  hvpncan 9183  hvaddsub4 9221  his5 9229  his2sub 9234  bcsiALT 9322  norm1 9397  hhssmetdval 9425  chocunii 9448  pjthlem7 9501  pjthlem8 9502  pjspansn 9776  fh1 9837  fh2 9838  cm2j 9839  5oalem2 9878  5oalem3 9879  5oalem5 9881  3oalem2 9886  pjvi 9928  mayete3i 9951  mayete3OLDi 9952  hoaddid1i 9992  hosubid1 10004  hoadddi 10009  honegsubdi2 10017  hoaddsub 10022  unoplin 10124  counop 10125  hmoplin 10146  hmopco 10227  nlelshi 10272  riesz3i 10274  adjcoi 10312  branmfn 10317  branmfnOLD 10318  kbass2 10330  kbass6 10334  hmopidmpji 10360  pjssposi 10380  pjclem4 10408  pj3si 10416  strlem1 10458  stcltrlem1 10484  mdexchi 10543  irredlem2 10600  ghomf1olem 10681  cayleylem2 10695  infi1 10735  moec 10745  opreq123d 10777  imrescl 10807  imfstnrelc 10810  toplat 10884  seqzp2 10918  multinv 10959  mult2inv 10961  sallnei 11016  limfillem2 11102  singcon 11137  2wsms 11153  1cat 11213  extrdom 11236  extrcod 11237  extrcmp 11238  extrid 11239  isfuna 11288  idsubfun 11312  subcld 11480  cnsubsp2 11484  compsublem 11487  compsub 11488  compfipin0lem 11492  compfipin0 11493  isufil2 11650  ufileu 11658  filufint 11659  fclsfnflim 11726  flimfnfcls 11727  fcluscnp 11730  gaid 11776  ssga 11777  ifbieq12d 11803  upxp 11822  upixp 11823  divexp 11859  rddif 11869  fsumlt1 11894  mettrifi2 11913  geomcau 11914  lmclim2 11915  iccst 11939  lincmb01cmp 11942  paste 11954  txuni 11975  uptx 11978  txcnopab 11980  heiborlem32 12042  heiborlem33 12043  bfplem6 12059  bfplem7 12060  bfplem8 12061  recms 12066  rrntotbndlem2 12077  phtpycolem4 12096

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 999  ax-17 1007  ax-4 1009  ax-5o 1011  ax-ext 1500

This theorem depends on definitions:  df-bi 145  df-an 223  df-cleq 1511

Copyright terms: Public domain