Theorem eqtr3d 2266

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

Syntax hints:   -> wi 4   = wceq 1397

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 1495  ax-gen 1497  ax-4 1558  ax-17 1574  ax-ext 2213

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

This theorem is referenced by:  3eqtr3d  2272  3eqtr3rd  2273  3eqtr3a  2288  opth  4329  eusvnf  4550  f00  5528  f1imacnv  5600  foimacnv  5601  f1ococnv1  5612  funfvdm  5709  fvmptdf  5734  fndmdif  5752  funopsn  5830  acexmidlemph  6011  acexmidlemab  6012  ovmpodf  6153  fvmpopr2d  6158  oprssov  6164  tfrlemisucaccv  6491  tfr1onlemsucaccv  6507  tfrcllemsucaccv  6520  oav2  6631  omv2  6633  fnsnsplitdc  6673  ecopovtrn  6801  ecopovtrng  6804  map0b  6856  en1  6973  ssenen  7037  fidifsnen  7057  dif1en  7068  undifdc  7116  fidcenumlemr  7154  ordiso2  7234  nninfninc  7322  nnnninfeq2  7328  nninfisollemne  7330  finomni  7339  exmidomni  7341  fodjum  7345  exmidaclem  7423  distrnqg  7607  1qec  7608  prarloclemarch2  7639  nnnq0lem1  7666  nqpnq0nq  7673  distrnq0  7679  prarloclemlt  7713  prmuloclemcalc  7785  ltaprg  7839  prplnqu  7840  recexprlem1ssl  7853  recexprlem1ssu  7854  ltmprr  7862  cauappcvgprlemopl  7866  caucvgprlemopl  7889  caucvgprprlemopl  7917  caucvgprprlemexb  7927  prsrlem1  7962  ltsosr  7984  mulgt0sr  7998  recidpipr  8076  recriota  8110  nntopi  8114  axcaucvglemres  8119  addlid  8318  readdcan  8319  muladd11r  8335  add32r  8339  cnegexlem2  8355  cnegex  8357  pncan2  8386  addsubass  8389  subadd23  8391  addsub12  8392  subid  8398  subid1  8399  npncan  8400  nppcan3  8403  subsub  8409  nppcan2  8410  nnncan2  8416  npncan3  8417  pnpcan  8418  negdi  8436  mvlraddd  8543  mvlladdd  8544  pnpncand  8554  subdi  8564  mulsub  8580  mulsub2  8581  eqord1  8663  recexap  8833  div32ap  8872  divsubdirap  8888  divmuldivap  8892  divdivdivap  8893  divmuleqap  8897  divcanap6  8899  dmdcanap  8902  divsubdivap  8908  div2negap  8915  div2subap  9017  mvllmulapd  9022  prodgt0gt0  9031  cju  9141  zneo  9581  infrenegsupex  9828  qreccl  9876  mul2lt0rlt0  9994  xnpcan  10107  fzosn  10451  modqid  10612  modqm1p1mod0  10638  modqltm1p1mod  10639  modqmul1  10640  modaddmodup  10650  modaddmodlo  10651  modqsubdir  10656  iseqf1olemkle  10760  iseqf1olemklt  10761  seq3f1olemstep  10777  seq3f1oleml  10779  seqf1oglem2  10783  seqfeq3  10792  seq3distr  10795  expineg2  10811  expm1t  10830  expadd  10844  expaddzaplem  10845  expmulzap  10848  sqsubswap  10862  subsq2  10910  binom2sub  10916  binom3  10920  facndiv  11002  bcval5  11026  bcn2p1  11033  bcnm1  11035  pfxccatpfx2  11322  2shfti  11409  shftcan2  11413  reim0  11439  imval2  11472  cjreim2  11482  cjdivap  11487  cnrecnv  11488  rennim  11580  resqrexlemnm  11596  remsqsqrt  11610  sqrtdiv  11620  sqrtmsq  11623  sqabsadd  11633  sqabssub  11634  absreim  11646  absdivap  11648  absnid  11651  sqabs  11660  abslt  11666  absle  11667  recvalap  11675  abssub  11679  maxabslemlub  11785  infxrnegsupex  11841  mulcn2  11890  reccn2ap  11891  cjcn2  11894  summodclem3  11959  summodclem2a  11960  summodc  11962  zsumdc  11963  fsum3  11966  fisumss  11971  fsumcl2lem  11977  fsumm1  11995  fsum1p  11997  isummulc2  12005  telfsumo  12045  binomlem  12062  bcxmas  12068  arisum  12077  trireciplem  12079  trirecip  12080  geolim2  12091  georeclim  12092  cvgratnnlemfm  12108  cvgratz  12111  mertenslemi1  12114  clim2divap  12119  prodmodclem3  12154  prodmodclem2a  12155  zproddc  12158  fprodseq  12162  fprodssdc  12169  fprod1p  12178  efcan  12255  efexp  12261  efzval  12262  efgt0  12263  eftlub  12269  efltim  12277  resinval  12294  recosval  12295  cosmul  12324  cos2t  12329  cos2tsin  12330  cos01bnd  12337  cos12dec  12347  eirraplem  12356  muldvds1  12395  dvdsexp  12440  oexpneg  12456  divalglemqt  12498  divalglemeunn  12500  divalglemeuneg  12502  divalgmod  12506  flodddiv4t2lthalf  12518  bitsmod  12535  bitsinv1lem  12540  gcdid0  12569  gcdaddm  12573  dvdsgcdidd  12583  rpmulgcd  12615  sqgcd  12618  algcvg  12638  eucalgcvga  12648  eucalg  12649  dvdslcm  12659  lcmeq0  12661  lcmgcd  12668  qredeu  12687  sqnprm  12726  divgcdodd  12733  sqrt2irrlem  12751  sqpweven  12765  2sqpwodd  12766  divnumden  12786  hashdvds  12811  phimullem  12815  eulerthlemrprm  12819  eulerthlemth  12822  odzdvds  12836  pythagtriplem3  12858  pythagtriplem4  12859  pythagtriplem14  12868  pythagtriplem19  12873  pcpremul  12884  pceulem  12885  pcqdiv  12898  pcaddlem  12930  fldivp1  12939  1arithlem4  12957  4sqlem10  12978  mul4sqlem  12984  4sqlem11  12992  4sqlem15  12996  4sqlem16  12997  4sqlem17  12998  ennnfonelemhf1o  13052  strslssd  13147  ressbas2d  13169  ressinbasd  13175  topnidg  13353  lidrideqd  13482  grpidd  13484  grprida  13488  gsumress  13496  ismndd  13538  grpidd2  13642  grpinvid1  13653  grpinvid2  13654  grppnpcan2  13695  grpnpncan  13696  dfgrp3mlem  13699  grpsubpropd2  13706  mhmid  13720  mhmmnd  13721  mulgsubcl  13741  mulgneg  13745  mulgaddcomlem  13750  mulginvinv  13753  mulgdirlem  13758  mulgdir  13759  mulgass  13764  mulgmodid  13766  grpissubg  13799  eqgcpbl  13833  ghmid  13854  ghmmulg  13861  resghm  13865  invghm  13934  gsumfzmptfidmadd  13944  mgptopng  13961  srgisid  14018  ringidss  14061  ringcom  14063  opprsubgg  14116  unitgrp  14149  1rinv  14161  0unit  14162  rhmdvdsr  14208  lringuplu  14229  subrngpropd  14249  subrgpropd  14286  lmod0vs  14354  lmodvsmmulgdi  14356  lmodvneg1  14363  lmodcom  14366  lmodsubvs  14376  lmodsubdir  14378  lmodpropd  14382  lspsnsub  14454  lspsneq0b  14460  lsppropd  14465  rlmscabas  14493  lidlbas  14511  zringmulg  14631  restopnb  14924  txcnmpt  15016  cnmpt1t  15028  blhalf  15151  xmspropd  15220  mspropd  15221  mpomulcn  15309  ivthreinc  15388  limcimolemlt  15407  dvfre  15453  dveflem  15469  dvef  15470  ply1termlem  15485  plymullem1  15491  sin2kpi  15554  cos2kpi  15555  sin2pim  15556  cos2pim  15557  ptolemy  15567  sincosq2sgn  15570  sincosq3sgn  15571  sincosq4sgn  15572  sinq12gt0  15573  tangtx  15581  sincosq1eq  15582  abssinper  15589  sinkpi  15590  relogeftb  15608  relogoprlem  15611  relogexp  15615  mpodvdsmulf1o  15733  mersenne  15740  perfectlem1  15742  perfectlem2  15743  perfect  15744  lgsval2lem  15758  lgsdir2lem4  15779  lgsdirprm  15782  lgsdilem2  15784  gausslemma2dlem7  15816  lgseisenlem4  15821  lgsquadlem1  15825  lgsquadlem2  15826  lgsquad2lem1  15829  lgsquad2lem2  15830  2sqlem4  15866  2sqlem6  15868  2sqlem8  15871  clwwlknonel  16302  eupth2fi  16349  peano3nninf  16660  nninfsel  16670  nninffeq  16673  isomninnlem  16685  cvgcmp2nlemabs  16687  trilpolemlt1  16696  trirec0xor  16700  qdiff  16704  ismkvnnlem  16708  gfsum0  16734