Theorem eqtr3d 2264

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

Hypotheses

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

Assertion

Ref	Expression
eqtr3d	|- ( ph -> B = C )

Proof of Theorem eqtr3d

Step	Hyp	Ref	Expression
1		eqtr3d.1	. . 3 |- ( ph -> A = B )
2	1	eqcomd 2235	. 2 |- ( ph -> B = A )
3		eqtr3d.2	. 2 |- ( ph -> A = C )
4	2, 3	eqtrd 2262	1 |- ( ph -> B = C )

Syntax hints:   -> wi 4   = wceq 1395

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1493  ax-gen 1495  ax-4 1556  ax-17 1572  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-cleq 2222

This theorem is referenced by:  3eqtr3d  2270  3eqtr3rd  2271  3eqtr3a  2286  opth  4323  eusvnf  4544  f00  5519  f1imacnv  5591  foimacnv  5592  f1ococnv1  5603  funfvdm  5699  fvmptdf  5724  fndmdif  5742  funopsn  5819  acexmidlemph  6000  acexmidlemab  6001  ovmpodf  6142  fvmpopr2d  6147  oprssov  6153  tfrlemisucaccv  6477  tfr1onlemsucaccv  6493  tfrcllemsucaccv  6506  oav2  6617  omv2  6619  fnsnsplitdc  6659  ecopovtrn  6787  ecopovtrng  6790  map0b  6842  en1  6959  ssenen  7020  fidifsnen  7040  dif1en  7049  undifdc  7097  fidcenumlemr  7133  ordiso2  7213  nninfninc  7301  nnnninfeq2  7307  nninfisollemne  7309  finomni  7318  exmidomni  7320  fodjum  7324  exmidaclem  7401  distrnqg  7585  1qec  7586  prarloclemarch2  7617  nnnq0lem1  7644  nqpnq0nq  7651  distrnq0  7657  prarloclemlt  7691  prmuloclemcalc  7763  ltaprg  7817  prplnqu  7818  recexprlem1ssl  7831  recexprlem1ssu  7832  ltmprr  7840  cauappcvgprlemopl  7844  caucvgprlemopl  7867  caucvgprprlemopl  7895  caucvgprprlemexb  7905  prsrlem1  7940  ltsosr  7962  mulgt0sr  7976  recidpipr  8054  recriota  8088  nntopi  8092  axcaucvglemres  8097  addlid  8296  readdcan  8297  muladd11r  8313  add32r  8317  cnegexlem2  8333  cnegex  8335  pncan2  8364  addsubass  8367  subadd23  8369  addsub12  8370  subid  8376  subid1  8377  npncan  8378  nppcan3  8381  subsub  8387  nppcan2  8388  nnncan2  8394  npncan3  8395  pnpcan  8396  negdi  8414  mvlraddd  8521  mvlladdd  8522  pnpncand  8532  subdi  8542  mulsub  8558  mulsub2  8559  eqord1  8641  recexap  8811  div32ap  8850  divsubdirap  8866  divmuldivap  8870  divdivdivap  8871  divmuleqap  8875  divcanap6  8877  dmdcanap  8880  divsubdivap  8886  div2negap  8893  div2subap  8995  mvllmulapd  9000  prodgt0gt0  9009  cju  9119  zneo  9559  infrenegsupex  9801  qreccl  9849  mul2lt0rlt0  9967  xnpcan  10080  fzosn  10423  modqid  10583  modqm1p1mod0  10609  modqltm1p1mod  10610  modqmul1  10611  modaddmodup  10621  modaddmodlo  10622  modqsubdir  10627  iseqf1olemkle  10731  iseqf1olemklt  10732  seq3f1olemstep  10748  seq3f1oleml  10750  seqf1oglem2  10754  seqfeq3  10763  seq3distr  10766  expineg2  10782  expm1t  10801  expadd  10815  expaddzaplem  10816  expmulzap  10819  sqsubswap  10833  subsq2  10881  binom2sub  10887  binom3  10891  facndiv  10973  bcval5  10997  bcn2p1  11004  bcnm1  11006  pfxccatpfx2  11284  2shfti  11357  shftcan2  11361  reim0  11387  imval2  11420  cjreim2  11430  cjdivap  11435  cnrecnv  11436  rennim  11528  resqrexlemnm  11544  remsqsqrt  11558  sqrtdiv  11568  sqrtmsq  11571  sqabsadd  11581  sqabssub  11582  absreim  11594  absdivap  11596  absnid  11599  sqabs  11608  abslt  11614  absle  11615  recvalap  11623  abssub  11627  maxabslemlub  11733  infxrnegsupex  11789  mulcn2  11838  reccn2ap  11839  cjcn2  11842  summodclem3  11906  summodclem2a  11907  summodc  11909  zsumdc  11910  fsum3  11913  fisumss  11918  fsumcl2lem  11924  fsumm1  11942  fsum1p  11944  isummulc2  11952  telfsumo  11992  binomlem  12009  bcxmas  12015  arisum  12024  trireciplem  12026  trirecip  12027  geolim2  12038  georeclim  12039  cvgratnnlemfm  12055  cvgratz  12058  mertenslemi1  12061  clim2divap  12066  prodmodclem3  12101  prodmodclem2a  12102  zproddc  12105  fprodseq  12109  fprodssdc  12116  fprod1p  12125  efcan  12202  efexp  12208  efzval  12209  efgt0  12210  eftlub  12216  efltim  12224  resinval  12241  recosval  12242  cosmul  12271  cos2t  12276  cos2tsin  12277  cos01bnd  12284  cos12dec  12294  eirraplem  12303  muldvds1  12342  dvdsexp  12387  oexpneg  12403  divalglemqt  12445  divalglemeunn  12447  divalglemeuneg  12449  divalgmod  12453  flodddiv4t2lthalf  12465  bitsmod  12482  bitsinv1lem  12487  gcdid0  12516  gcdaddm  12520  dvdsgcdidd  12530  rpmulgcd  12562  sqgcd  12565  algcvg  12585  eucalgcvga  12595  eucalg  12596  dvdslcm  12606  lcmeq0  12608  lcmgcd  12615  qredeu  12634  sqnprm  12673  divgcdodd  12680  sqrt2irrlem  12698  sqpweven  12712  2sqpwodd  12713  divnumden  12733  hashdvds  12758  phimullem  12762  eulerthlemrprm  12766  eulerthlemth  12769  odzdvds  12783  pythagtriplem3  12805  pythagtriplem4  12806  pythagtriplem14  12815  pythagtriplem19  12820  pcpremul  12831  pceulem  12832  pcqdiv  12845  pcaddlem  12877  fldivp1  12886  1arithlem4  12904  4sqlem10  12925  mul4sqlem  12931  4sqlem11  12939  4sqlem15  12943  4sqlem16  12944  4sqlem17  12945  ennnfonelemhf1o  12999  strslssd  13094  ressbas2d  13116  ressinbasd  13122  topnidg  13300  lidrideqd  13429  grpidd  13431  grprida  13435  gsumress  13443  ismndd  13485  grpidd2  13589  grpinvid1  13600  grpinvid2  13601  grppnpcan2  13642  grpnpncan  13643  dfgrp3mlem  13646  grpsubpropd2  13653  mhmid  13667  mhmmnd  13668  mulgsubcl  13688  mulgneg  13692  mulgaddcomlem  13697  mulginvinv  13700  mulgdirlem  13705  mulgdir  13706  mulgass  13711  mulgmodid  13713  grpissubg  13746  eqgcpbl  13780  ghmid  13801  ghmmulg  13808  resghm  13812  invghm  13881  gsumfzmptfidmadd  13891  mgptopng  13907  srgisid  13964  ringidss  14007  ringcom  14009  opprsubgg  14062  unitgrp  14095  1rinv  14107  0unit  14108  rhmdvdsr  14154  lringuplu  14175  subrngpropd  14195  subrgpropd  14232  lmod0vs  14300  lmodvsmmulgdi  14302  lmodvneg1  14309  lmodcom  14312  lmodsubvs  14322  lmodsubdir  14324  lmodpropd  14328  lspsnsub  14400  lspsneq0b  14406  lsppropd  14411  rlmscabas  14439  lidlbas  14457  zringmulg  14577  restopnb  14870  txcnmpt  14962  cnmpt1t  14974  blhalf  15097  xmspropd  15166  mspropd  15167  mpomulcn  15255  ivthreinc  15334  limcimolemlt  15353  dvfre  15399  dveflem  15415  dvef  15416  ply1termlem  15431  plymullem1  15437  sin2kpi  15500  cos2kpi  15501  sin2pim  15502  cos2pim  15503  ptolemy  15513  sincosq2sgn  15516  sincosq3sgn  15517  sincosq4sgn  15518  sinq12gt0  15519  tangtx  15527  sincosq1eq  15528  abssinper  15535  sinkpi  15536  relogeftb  15554  relogoprlem  15557  relogexp  15561  mpodvdsmulf1o  15679  mersenne  15686  perfectlem1  15688  perfectlem2  15689  perfect  15690  lgsval2lem  15704  lgsdir2lem4  15725  lgsdirprm  15728  lgsdilem2  15730  gausslemma2dlem7  15762  lgseisenlem4  15767  lgsquadlem1  15771  lgsquadlem2  15772  lgsquad2lem1  15775  lgsquad2lem2  15776  2sqlem4  15812  2sqlem6  15814  2sqlem8  15817  peano3nninf  16433  nninfsel  16443  nninffeq  16446  isomninnlem  16458  cvgcmp2nlemabs  16460  trilpolemlt1  16469  trirec0xor  16473  ismkvnnlem  16480