Theorem eqtr4d 1510

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 1480	. 2 |- (ph -> B = C)
4	1, 3	eqtrd 1507	1 |- (ph -> A = C)

Syntax hints:   -> wi 3   = wceq 956

This theorem is referenced by:  3eqtr2d 1513  3eqtr2rd 1514  3eqtr4d 1517  3eqtr4rd 1518  ifswap 2382  opthwiener 2807  relop 3275  relimasn 3425  f1ococnv2 3708  fveqres 3749  funfv 3770  fvco 3774  fsn2 3836  fconst2g 3845  ndmoprcom 4047  ndmoprass 4048  ndmoprdistr 4049  1stval 4081  2ndval 4082  1st2val 4095  2nd2val 4096  curry1val 4100  oev2 4162  oesuc 4166  oaass 4195  odi 4210  omass 4211  oewordi 4218  oewordri 4219  oelim2 4222  nnacom 4233  nnmsucr 4240  nnmcom 4241  fundmen 4428  pw2en 4446  xpmapenlem3 4498  ranklim 4685  rankuni 4698  cardval 4826  cfsuc 4915  distrpq 5067  recmulpq 5070  addcompr 5123  mulcompr 5125  mulcmpblnrlem 5182  0idsr 5206  1idsr 5207  cnegext 5348  mulneg12t 5453  subsub3t 5463  subadd4t 5475  mulsubt 5477  recextlem1 5682  halfaddsubt 6041  supxrre 6083  zaddclt 6165  uzrdgsuc 6304  shftval2t 6347  shftval4t 6349  seqzfval2 6538  seq1seq0 6545  mulexpt 6594  recexpt 6595  expaddt 6596  expmult 6597  divexpt 6599  expword2it 6605  subsqt 6642  bernneq 6652  nn0opth 6666  cjexpt 6817  abscjt 6834  absret 6866  absmaxt 6897  abs1m 6904  caure 6927  cauim 6928  facp1t 6936  faclbnd 6945  faclbnd6 6954  bccmplt 6962  sumeq2 6985  fsum1ps 7018  fsumsplit 7020  fsumconst 7038  serzmulc1 7057  binomlem2 7067  iserzshft2 7107  climrecl 7110  climaddc1 7118  climsub 7130  climsubc2 7131  caucvg3a 7164  caucvg3lem 7166  ser1cmp2 7177  iserzabslem 7178  isumshft 7204  isumshft2 7205  isummulc1ALT 7213  infcvglem2 7222  geolimilem 7235  0.999... 7246  cvgratlem2ALT 7248  cvgratlem2 7251  negfcncf 7269  mulc1cncf 7279  efcltlem1 7304  dfef2 7307  erelem2 7320  efaddlem26 7363  efsubt 7371  ef1tllem 7381  ef01tllem1 7383  eirrlem2 7390  efi4pt 7435  sinnegt 7442  subcost 7460  sincossqt 7461  cos2tt 7463  demoivre 7484  iscncl 7770  ioo2bl 7912  xplmi 7973  fsumcnlem 7989  bcthlem1 7999  grpidinv2 8060  grpinv 8069  grp2inv 8078  grpinvf 8079  grpinvdiv 8084  grpsn 8124  ablsn 8125  ghgrpilem1 8133  ghsubgi 8138  ringsn 8163  vcoprne 8198  bafval 8223  nvmfval 8264  nvge0 8302  imsmetlem 8323  ipval2 8357  ipval3 8359  ip0r 8370  ip1cnilem6 8378  sspmlem 8391  lnocoi 8418  nvcnpi3 8422  nvcnpi4 8423  nmlno0lem 8453  blometi 8463  ipasslem1 8490  ipasslem11 8500  ipblnfi 8516  minveclem9 8553  minveclem18 8562  minveclem19 8563  minveclem30 8574  minveclem35 8579  minveclem36 8580  minveclem38 8582  sinco 8667  cosco 8668  sinperlem1 8686  efimpi 8698  shftefif1olem 8741  hvsub4t 8906  hvsubdistr2t 8917  his5t 8953  hhip 9044  pjpot 9261  shscl 9281  hsupvalt 9301  shjcomt 9330  h1de2b 9477  normcant 9499  spanunsn 9502  cm0t 9552  dfiop2 9679  hocadddir 9705  hocsubdir 9706  honegsub 9722  homco1t 9727  homulasst 9728  hoadddit 9729  hoadddirt 9730  hosubadd4t 9740  eigorth 9763  brafnmult 9875  kbmult 9879  0hmop 9907  0lnfn 9909  adj0 9919  nmlnop0ALT 9920  lnopm 9925  hmopcot 9948  riesz3 9995  cnlnadjlem6 10005  adjlnopt 10019  nmopadjle 10021  adjaddt 10026  nmopco 10028  nmopcoadj 10034  kbass1t 10049  kbass2t 10050  kbass4t 10052  kbass6t 10054  leopsqt 10062  leopnmidt 10071  pjscj 10098  pjinvar 10119  superpos 10281  atord 10311  atcvat3 10323  dmdbr6at 10350  cdj3lem1 10361  ghomsn 10388  hmeogrp 10538  mslb1 10629  cnvtr 10638  cmpassoh 10729  homgrf 10730

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 963  ax-17 971  ax-4 973  ax-5o 975  ax-ext 1459

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

Copyright terms: Public domain