Theorem eqtr4d 1928

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

Syntax hints:   -> wi 3   = wceq 1298

This theorem is referenced by:  3eqtr2d 1932  3eqtr2rd 1933  3eqtr4d 1937  3eqtr4dOLD 1938  3eqtr4rd 1939  3eqtr4a 1954  ifswap 3010  opthwiener 3554  onsucuni2 3914  relop 4113  relimasn 4288  dmsnopOLD 4368  f1ococnv2 4662  nfunsnOLD 4707  fveqres 4708  funfv 4731  dffv2 4734  fvco 4736  fsn2 4809  fconst2g 4821  ndmoprcom 4980  ndmoprass 4981  ndmoprdistr 4982  1stval 5022  2ndval 5023  1st2val 5038  2nd2val 5039  curry1val 5077  curry2val 5080  fparlem3 5083  fparlem4 5084  iotaequ 5097  oev2 5207  oesuc 5211  oaass 5243  odi 5258  omass 5259  oewordi 5266  oewordri 5267  oelim2 5270  oeoalem 5271  oeoa 5272  oeoelem 5273  oeoe 5274  nnacom 5288  nnmsucrOLD 5296  nnmcom 5297  nnmcomOLD 5298  fundmen 5487  pw2en 5505  riotav 5565  riotabidva 5575  xpmapenlem3 5592  ranklim 5796  rankuni 5809  cardsucnn 5871  cardval 5975  cfsuc 6063  nnacda 6088  distrpq 6219  recmulpq 6222  addcompr 6275  mulcompr 6277  mulcmpblnrlem 6334  0idsr 6358  1idsr 6359  cnegex 6502  mulneg12 6617  subsub3 6628  subadd4 6642  mulsub 6644  recextlem1 6874  halfaddsub 7227  supxrre 7292  zaddcl 7374  modcyc 7516  modcyc2 7517  modmul1 7519  uzrdgsuci 7716  cardfz 7719  shftval2 7760  shftval4 7762  seqzfval2 7781  seq1seq0 7788  mulexp 7836  exprec 7837  exprecOLD 7838  expadd 7839  expmul 7840  expdiv 7844  expword2i 7850  subsq 7888  bernneq 7898  bernneqOLD 7899  digit2 7904  nn0opthi 7916  cjexp 8067  abscj 8085  absre 8117  absmax 8149  abs1mi 8156  caurei 8179  cauimi 8180  facp1 8188  faclbnd 8197  faclbnd6 8206  bccmpl 8214  hashgval 8230  sumeq2 8245  fsum1ps 8278  fsumsplit 8280  fsumconst 8298  serzmulc1 8317  binomlem2 8327  iserzshft2i 8367  climrecl 8370  climaddc1 8378  climsub 8390  climsubc2 8391  caucvg3ai 8424  caucvg3lem 8426  ser1cmp2i 8437  iserzabslem 8438  isumshfti 8465  isumshft2i 8466  isummulc1iALT 8474  infcvglem2 8483  geolimilem 8497  0.999... 8508  cvgratlem2ALT 8510  cvgratlem2 8513  negfcncfi 8531  mulc1cncf 8541  efcltlem1 8566  dfef2i 8569  erelem2 8582  efaddlem26 8625  efsub 8633  ef1tllem 8643  ef01tllem1 8645  eirrlem2 8652  efi4p 8700  sinneg 8707  subcos 8725  sincossq 8726  cos2t 8728  demoivre 8752  iscncl 9047  ioo2bl 9190  xplmi 9251  fsumcnlem 9267  bcthlem1 9277  grpsn 9340  grpidinv2 9344  grpinv 9353  grp2inv 9363  grpinvf 9364  grpinvdiv 9369  gxnn0neg 9386  gxnn0suc 9387  gxcom 9392  gxinv 9393  gxdi 9422  ablsn 9433  ghgrpilem1 9441  ghsubgi 9446  ringsn 9490  vcoprne 9530  bafval 9555  nvmfval 9596  nvge0 9634  imsmetlem 9655  ipval2 9696  ipval3 9698  ip0r 9709  ip1cnilem6 9717  sspmlem 9730  lnocoi 9757  nvcnpi3 9761  nvcnpi4 9762  nmlno0lem 9793  blometi 9803  ipasslem1 9831  ipasslem11 9841  ipblnfi 9857  minveclem9 9898  minveclem18 9907  minveclem19 9908  minveclem30 9919  minveclem35 9924  minveclem36 9925  minveclem38 9927  sinco 10016  cosco 10017  sinperlem1 10035  efimpi 10047  shftefif1olem 10095  upxp 10225  hvsub4 10538  hvsubdistr2 10549  his5 10586  hhip 10677  pjpo 10894  shscli 10914  hsupval 10934  shjcom 10963  h1de2bi 11110  normcan 11132  spanunsni 11135  cm0 11185  dfiop2 11316  hocadddiri 11342  hocsubdiri 11343  honegsubi 11359  homco1 11364  homulass 11365  hoadddi 11366  hoadddir 11367  hosubadd4 11377  eigorthi 11400  brafnmul 11512  kbmul 11516  0hmop 11544  0lnfn 11546  adj0 11556  nmlnop0iALT 11557  lnopmi 11562  hmopco 11585  riesz3i 11632  cnlnadjlem6 11642  adjlnop 11656  nmopadjlei 11658  adjadd 11663  nmopcoi 11665  nmopcoadji 11671  kbass1 11687  kbass2 11688  kbass4 11690  kbass6 11692  leopsq 11700  leopnmid 11709  pjscji 11742  pjinvari 11764  superpos 11926  atordi 11956  atcvat3i 11968  dmdbr6ati 11995  cdj3lem1 12006  bnj583 13296  bnj1321 13498  bnj1501 13570  modaddabs 13612  ghomsn 13631  divalgmod 13709  gcd0id 13729  gcdneg 13732  gcdaddmlem 13734  modgcd 13738  mulgcdlem2 13757  axfelem8 14038  axfelem9 14039  dranfldrefc 14363  cur1vald 14547  prodeq2 14661  relsumprd 14684  ltlga 14729  fprodsub 14742  trinv 14759  rngunval2 14774  muldisc 14824  hmeogrp 14892  mslb1 15007  cnvtr 15016  dualcat2 15133  cmpassoh 15150  homgrf 15151  idsubfun 15206  fictb 15371  cptclsscpt 15432  compfipin0lem 15435  compfipin0 15436  ivthALT 15454  limfilcf 15587  rnelfmlem 15592  fmfnfmlem3 15596  fvif 15692  ifeq1da 15693  ifeq2da 15694  rddif 15798  sdclem1 15809  fsumlt1 15831  csbrni 15832  geomcau 15849  piececn 15894  sstotbnd 15936  bfplem8 16005  rrntotbndlem2 16021  rrntotbnd 16022  iccbnd 16026  phtpycolem4 16054  reparpht 16065  pcoass 16085  pcorevlem 16086  pcorev 16087  pi1gp 16095  pi1set 16096  ringsubdi 16106  ringsubdir 16107  omllaw3 16966  cmt2 16971  glbcon 17028  cvrat3 17075  grpidinv2NEW 17119  grpinvNEW 17128  divrngidNEW 17166  pmap1 17247  pmapglbx 17251  pmapglb2 17253  pmapglb2x 17254  paddasslem17 17297  paddun 17337  poml4 17361

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1305  ax-17 1317  ax-4 1319  ax-5o 1321  ax-ext 1865

This theorem depends on definitions:  df-bi 164  df-an 242  df-cleq 1877

Copyright terms: Public domain