Theorem eqtr4d 1508

Description: An equality transitivity equality deduction.

Hypotheses

Ref	Expression
eqtr4d.1	|- (ph -> A = B)
eqtr4d.2	|- (ph -> C = B)

Assertion

Ref	Expression
eqtr4d	|- (ph -> A = C)

Proof of Theorem eqtr4d

Step	Hyp	Ref	Expression
1		eqtr4d.1	. 2 |- (ph -> A = B)
2		eqtr4d.2	. . 3 |- (ph -> C = B)
3	2	eqcomd 1478	. 2 |- (ph -> B = C)
4	1, 3	eqtrd 1505	1 |- (ph -> A = C)

Syntax hints:   -> wi 3   = wceq 955

This theorem is referenced by:  3eqtr2d 1511  3eqtr2rd 1512  3eqtr4d 1515  3eqtr4rd 1516  ifswap 2379  opthwiener 2803  relop 3271  relimasn 3421  f1ococnv2 3703  fveqres 3744  funfv 3765  fvco 3769  fsn2 3831  fconst2g 3840  ndmoprcom 4042  ndmoprass 4043  ndmoprdistr 4044  1stval 4074  2ndval 4075  1st2val 4088  2nd2val 4089  curry1val 4093  oev2 4155  oesuc 4159  oaass 4188  odi 4203  omass 4204  oewordi 4211  oewordri 4212  oelim2 4215  nnacom 4226  nnmsucr 4233  nnmcom 4234  fundmen 4418  pw2en 4435  xpmapenlem3 4487  ranklim 4668  rankuni 4681  cardval 4809  cfsuc 4898  distrpq 5050  recmulpq 5053  addcompr 5106  mulcompr 5108  mulcmpblnrlem 5165  0idsr 5189  1idsr 5190  cnegext 5331  mulneg12t 5436  subsub3t 5446  subadd4t 5458  mulsubt 5460  recextlem1 5665  halfaddsubt 5998  supxrre 6040  zaddclt 6122  uzrdgsuc 6254  shftval2t 6297  shftval4t 6299  seqzfval2 6483  seq1seq0 6490  mulexpt 6539  recexpt 6540  expaddt 6541  expmult 6542  divexpt 6544  expword2it 6550  subsqt 6587  bernneq 6597  nn0opth 6611  imret 6725  cjexpt 6767  abscjt 6784  absret 6816  abs1m 6856  caure 6879  cauim 6880  facp1t 6888  faclbnd 6897  faclbnd6 6906  bccmplt 6915  sumeq2 6938  fsum1ps 6971  fsumsplit 6973  fsumconst 6991  serzmulc1 7010  binomlem2 7020  iserzshft2 7060  climrecl 7063  climaddc1 7071  climsub 7083  climsubc2 7084  caucvg3a 7117  caucvg3lem 7119  ser1cmp2 7130  iserzabslem 7131  isumshft 7156  isumshft2 7157  isummulc1ALT 7165  infcvglem2 7174  geolimilem 7187  0.999... 7198  cvgratlem2ALT 7200  cvgratlem2 7203  negfcncf 7221  mulc1cncf 7231  efcltlem1 7263  dfef2 7266  erelem2 7279  efaddlem26 7322  efsubt 7330  ef1tllem 7340  ef01tllem1 7342  eirrlem2 7348  efi4pt 7394  sinnegt 7401  efeult 7408  subcost 7419  sincossqt 7420  cos2tt 7422  demoivre 7443  iscncl 7730  ioo2bl 7874  xplmi 7935  fsumcnlem 7951  bcthlem1 7961  grpidinv2 8022  grpinv 8031  grp2inv 8040  grpinvf 8041  grpinvdiv 8046  grpsn 8088  ablsn 8089  ghgrpilem1 8097  ghsubgi 8102  ringsn 8127  vcoprne 8162  bafval 8187  nvmfval 8228  nvge0 8266  imsmetlem 8287  ipval2 8319  ipval3 8321  ip0r 8332  ip1cnilem6 8340  sspmlem 8353  lnocoi 8380  nvcnpi4 8383  nmlno0lem 8413  blometi 8422  ipasslem1 8449  ipasslem11 8459  ipblnfi 8475  minveclem9 8512  minveclem18 8521  minveclem19 8522  minveclem30 8533  minveclem35 8538  minveclem36 8539  minveclem38 8541  sinco 8621  cosco 8622  sinperlem1 8640  efimpi 8650  shftefif1olem 8696  hvsub4t 8861  hvsubdistr2t 8872  his5t 8908  hhip 8999  pjpot 9216  shscl 9236  hsupvalt 9256  shjcomt 9285  h1de2b 9432  h1de2bOLD 9433  normcant 9456  spanunsn 9459  cm0t 9509  dfiop2 9636  hocadddir 9662  hocsubdir 9663  honegsub 9679  homco1t 9684  homulasst 9685  hoadddit 9686  hoadddirt 9687  hosubadd4t 9697  eigorth 9720  brafnmult 9832  kbmult 9836  0hmop 9864  0lnfn 9866  adj0 9875  nmlnop0ALT 9876  lnopm 9881  hmopcot 9904  riesz3 9951  cnlnadjlem6 9961  adjlnopt 9975  nmopadjle 9977  adjaddt 9982  nmopco 9984  nmopcoadj 9990  kbass1t 10005  kbass2t 10006  kbass4t 10008  kbass6t 10010  leopsqt 10018  leopnmidt 10027  pjscj 10054  pjinvar 10075  superpos 10237  atord 10267  atcvat3 10279  dmdbr6at 10306  cdj3lem1 10317  ghomsn 10344  hmeogrp 10484  mslb1 10545  cnvtr 10554  cmpassoh 10645  homgrf 10646

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