Theorem eqtr4d 2201

Description: An equality transitivity equality deduction. (Contributed by NM, 18-Jul-1995.)

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

Syntax hints:   -> wi 4   = wceq 1343

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1435  ax-gen 1437  ax-4 1498  ax-17 1514  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-cleq 2158

This theorem is referenced by:  3eqtr2d  2204  3eqtr2rd  2205  3eqtr4d  2208  3eqtr4rd  2209  3eqtr4a  2224  sbnfc2  3104  ifsbdc  3531  ifeq1dadc  3549  eqifdc  3553  ifnotdc  3555  ifandc  3556  onsucuni2  4540  relop  4753  riinint  4864  iotauni  5164  fniinfv  5543  fsn2  5658  fmptapd  5675  fconst2g  5699  fniunfv  5729  ofres  6063  ofco  6067  frecsuclem  6370  frecrdg  6372  oasuc  6428  nnacom  6448  nnaass  6449  nndi  6450  nnmass  6451  nnmsucr  6452  nnmcom  6453  funresdfunsndc  6470  uniqs2  6557  en1bg  6762  fundmen  6768  1domsn  6781  mapxpen  6810  xpmapenlem  6811  phplem4dom  6824  en2eqpr  6869  sbthlemi5  6922  omp1eomlem  7055  difinfsnlem  7060  ctmlemr  7069  ctssdccl  7072  ctssdc  7074  infnninf  7084  infnninfOLD  7085  nnnninfeq  7088  exmidonfinlem  7145  addcmpblnq  7304  distrnqg  7324  ltexnqq  7345  addcmpblnq0  7380  nqnq0a  7391  nqnq0m  7392  nq0m0r  7393  nq0a0  7394  nnanq0  7395  distrnq0  7396  prarloclemlo  7431  prarloclemcalc  7439  genpassl  7461  genpassu  7462  ltsosr  7701  0idsr  7704  1idsr  7705  mulextsr1lem  7717  cnegex  8072  subsub3  8126  subadd4  8138  mulneg12  8291  mulsub  8295  apreap  8481  cru  8496  recextlem1  8544  cju  8852  halfaddsub  9087  nn0supp  9162  nneo  9290  zeo2  9293  uzin  9494  xaddcom  9793  xaddass  9801  xleaddadd  9819  iccf1o  9936  fzsuc2  10010  flqeqceilz  10249  zmod1congr  10272  modqcyc  10290  modqcyc2  10291  modqaddabs  10293  modqmul1  10308  modqaddmulmod  10322  addmodlteq  10329  frec2uzrdg  10340  frecuzrdgsuctlem  10354  seq3val  10389  seqvalcd  10390  seq3fveq2  10400  seq3split  10410  seq3distr  10444  ser0f  10446  expp1  10458  mulexp  10490  mulexpzap  10491  expadd  10493  expaddzap  10495  expmul  10496  expmulzap  10497  expsubap  10499  expdivap  10502  subsq  10557  mulbinom2  10567  binom3  10568  bernneq  10571  modqexp  10577  nn0opthd  10631  faclbnd  10650  faclbnd6  10653  bccmpl  10663  bcp1n  10670  zfz1isolemiso  10748  seq3coll  10751  shftval2  10764  shftval4  10766  seq3shft  10776  crre  10795  remim  10798  remullem  10809  cjexp  10831  cnrecnv  10848  resqrexlemlo  10951  resqrexlemcalc1  10952  resqrexlemcalc2  10953  resqrexlemcalc3  10954  resqrexlemnm  10956  rsqrmo  10965  abscj  10990  absid  11009  absre  11015  recvalap  11035  maxabsle  11142  maxltsup  11156  2zsupmax  11163  minabs  11173  bdtrilem  11176  bdtri  11177  2zinfmin  11180  xrmaxiflemab  11184  xrmaxiflemcom  11186  xrmaxadd  11198  xrbdtri  11213  iooinsup  11214  climaddc1  11266  climmulc2  11268  climsubc1  11269  climsubc2  11270  climcvg1nlem  11286  summodclem3  11317  zsumdc  11321  isum  11322  isumz  11326  isumss  11328  fisumss  11329  fsum3cvg2  11331  fsumadd  11343  isummulc2  11363  sumsplitdc  11369  fsum2dlemstep  11371  fisumcom2  11375  fisum0diag2  11384  fsumconst  11391  telfsumo  11403  fsumparts  11407  fsumrelem  11408  binomlem  11420  isumshft  11427  isumsplit  11428  arisum  11435  arisum2  11436  trireciplem  11437  geolim2  11449  geo2sum  11451  0.999...  11458  cvgratz  11469  mertensabs  11474  clim2prod  11476  prodf1f  11480  prodmodclem2a  11513  zproddc  11516  iprodap  11517  iprodap0  11519  fprodseq  11520  prod1dc  11523  prodssdc  11526  fprod2dlemstep  11559  fprodcom2fi  11563  fproddivap  11567  ef0lem  11597  efval2  11602  ege2le3  11608  efaddlem  11611  efsub  11618  eftlub  11627  efsep  11628  tanval3ap  11651  efi4p  11654  sinneg  11663  sinmul  11681  sincossq  11685  cos2t  11687  demoivreALT  11710  eirraplem  11713  dvdsmodexp  11731  odd2np1  11806  omoe  11829  divalglemex  11855  divalglemeuneg  11856  divalgmod  11860  flodddiv4  11867  gcdneg  11911  gcdaddm  11913  modgcd  11920  bezoutlemnewy  11925  gcdass  11944  gcdmultiple  11949  algrp1  11974  lcmneg  12002  lcmgcdeq  12011  lcmass  12013  cncongr2  12032  prmexpb  12079  sqrt2irr  12090  2sqpwodd  12104  qnumdenbi  12120  phiprmpw  12150  eulerthlema  12158  fermltl  12162  prmdiveq  12164  modprm0  12182  pythagtriplem1  12193  pythagtriplem12  12203  pythagtriplem14  12205  pythagtriplem15  12206  pythagtriplem16  12207  pythagtriplem17  12208  pythagtriplem19  12210  pcpremul  12221  pcneg  12252  pcgcd  12256  pc2dvds  12257  pcaddlem  12266  pcprod  12272  fldivp1  12274  pcbc  12277  prmpwdvds  12281  pockthlem  12282  mul4sqlem  12319  ctiunctlemfo  12368  strslfv3  12435  restuni2  12777  lmfval  12792  cnfval  12794  cnpfval  12795  txtopon  12862  txcnp  12871  upxp  12872  txrest  12876  cnmptcom  12898  bl2in  13003  xblss2  13005  isxms2  13052  setsmsdsg  13080  setsmstsetg  13081  metss  13094  resubmet  13148  cncfcncntop  13180  dvidlemap  13260  dvcnp2cntop  13263  dvcoapbr  13271  dvcjbr  13272  dvexp  13275  dvexp2  13276  dvrecap  13277  efimpi  13340  tangtx  13359  logdivlti  13402  cxpexprp  13416  rpcxpsub  13429  rpabscxpbnd  13459  rprelogbdiv  13475  binom4  13497  lgslem1  13501  lgsmod  13527  lgsdilem  13528  lgsdi  13538  lgsne0  13539  lgsdirnn0  13548  lgsdinn0  13549  2sqlem4  13554  bj-charfundcALT  13651  sssneq  13842  0nninf  13844  trilpolemisumle  13877