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  5829  acexmidlemph  6010  acexmidlemab  6011  ovmpodf  6152  fvmpopr2d  6157  oprssov  6163  tfrlemisucaccv  6490  tfr1onlemsucaccv  6506  tfrcllemsucaccv  6519  oav2  6630  omv2  6632  fnsnsplitdc  6672  ecopovtrn  6800  ecopovtrng  6803  map0b  6855  en1  6972  ssenen  7036  fidifsnen  7056  dif1en  7067  undifdc  7115  fidcenumlemr  7153  ordiso2  7233  nninfninc  7321  nnnninfeq2  7327  nninfisollemne  7329  finomni  7338  exmidomni  7340  fodjum  7344  exmidaclem  7422  distrnqg  7606  1qec  7607  prarloclemarch2  7638  nnnq0lem1  7665  nqpnq0nq  7672  distrnq0  7678  prarloclemlt  7712  prmuloclemcalc  7784  ltaprg  7838  prplnqu  7839  recexprlem1ssl  7852  recexprlem1ssu  7853  ltmprr  7861  cauappcvgprlemopl  7865  caucvgprlemopl  7888  caucvgprprlemopl  7916  caucvgprprlemexb  7926  prsrlem1  7961  ltsosr  7983  mulgt0sr  7997  recidpipr  8075  recriota  8109  nntopi  8113  axcaucvglemres  8118  addlid  8317  readdcan  8318  muladd11r  8334  add32r  8338  cnegexlem2  8354  cnegex  8356  pncan2  8385  addsubass  8388  subadd23  8390  addsub12  8391  subid  8397  subid1  8398  npncan  8399  nppcan3  8402  subsub  8408  nppcan2  8409  nnncan2  8415  npncan3  8416  pnpcan  8417  negdi  8435  mvlraddd  8542  mvlladdd  8543  pnpncand  8553  subdi  8563  mulsub  8579  mulsub2  8580  eqord1  8662  recexap  8832  div32ap  8871  divsubdirap  8887  divmuldivap  8891  divdivdivap  8892  divmuleqap  8896  divcanap6  8898  dmdcanap  8901  divsubdivap  8907  div2negap  8914  div2subap  9016  mvllmulapd  9021  prodgt0gt0  9030  cju  9140  zneo  9580  infrenegsupex  9827  qreccl  9875  mul2lt0rlt0  9993  xnpcan  10106  fzosn  10449  modqid  10610  modqm1p1mod0  10636  modqltm1p1mod  10637  modqmul1  10638  modaddmodup  10648  modaddmodlo  10649  modqsubdir  10654  iseqf1olemkle  10758  iseqf1olemklt  10759  seq3f1olemstep  10775  seq3f1oleml  10777  seqf1oglem2  10781  seqfeq3  10790  seq3distr  10793  expineg2  10809  expm1t  10828  expadd  10842  expaddzaplem  10843  expmulzap  10846  sqsubswap  10860  subsq2  10908  binom2sub  10914  binom3  10918  facndiv  11000  bcval5  11024  bcn2p1  11031  bcnm1  11033  pfxccatpfx2  11317  2shfti  11391  shftcan2  11395  reim0  11421  imval2  11454  cjreim2  11464  cjdivap  11469  cnrecnv  11470  rennim  11562  resqrexlemnm  11578  remsqsqrt  11592  sqrtdiv  11602  sqrtmsq  11605  sqabsadd  11615  sqabssub  11616  absreim  11628  absdivap  11630  absnid  11633  sqabs  11642  abslt  11648  absle  11649  recvalap  11657  abssub  11661  maxabslemlub  11767  infxrnegsupex  11823  mulcn2  11872  reccn2ap  11873  cjcn2  11876  summodclem3  11940  summodclem2a  11941  summodc  11943  zsumdc  11944  fsum3  11947  fisumss  11952  fsumcl2lem  11958  fsumm1  11976  fsum1p  11978  isummulc2  11986  telfsumo  12026  binomlem  12043  bcxmas  12049  arisum  12058  trireciplem  12060  trirecip  12061  geolim2  12072  georeclim  12073  cvgratnnlemfm  12089  cvgratz  12092  mertenslemi1  12095  clim2divap  12100  prodmodclem3  12135  prodmodclem2a  12136  zproddc  12139  fprodseq  12143  fprodssdc  12150  fprod1p  12159  efcan  12236  efexp  12242  efzval  12243  efgt0  12244  eftlub  12250  efltim  12258  resinval  12275  recosval  12276  cosmul  12305  cos2t  12310  cos2tsin  12311  cos01bnd  12318  cos12dec  12328  eirraplem  12337  muldvds1  12376  dvdsexp  12421  oexpneg  12437  divalglemqt  12479  divalglemeunn  12481  divalglemeuneg  12483  divalgmod  12487  flodddiv4t2lthalf  12499  bitsmod  12516  bitsinv1lem  12521  gcdid0  12550  gcdaddm  12554  dvdsgcdidd  12564  rpmulgcd  12596  sqgcd  12599  algcvg  12619  eucalgcvga  12629  eucalg  12630  dvdslcm  12640  lcmeq0  12642  lcmgcd  12649  qredeu  12668  sqnprm  12707  divgcdodd  12714  sqrt2irrlem  12732  sqpweven  12746  2sqpwodd  12747  divnumden  12767  hashdvds  12792  phimullem  12796  eulerthlemrprm  12800  eulerthlemth  12803  odzdvds  12817  pythagtriplem3  12839  pythagtriplem4  12840  pythagtriplem14  12849  pythagtriplem19  12854  pcpremul  12865  pceulem  12866  pcqdiv  12879  pcaddlem  12911  fldivp1  12920  1arithlem4  12938  4sqlem10  12959  mul4sqlem  12965  4sqlem11  12973  4sqlem15  12977  4sqlem16  12978  4sqlem17  12979  ennnfonelemhf1o  13033  strslssd  13128  ressbas2d  13150  ressinbasd  13156  topnidg  13334  lidrideqd  13463  grpidd  13465  grprida  13469  gsumress  13477  ismndd  13519  grpidd2  13623  grpinvid1  13634  grpinvid2  13635  grppnpcan2  13676  grpnpncan  13677  dfgrp3mlem  13680  grpsubpropd2  13687  mhmid  13701  mhmmnd  13702  mulgsubcl  13722  mulgneg  13726  mulgaddcomlem  13731  mulginvinv  13734  mulgdirlem  13739  mulgdir  13740  mulgass  13745  mulgmodid  13747  grpissubg  13780  eqgcpbl  13814  ghmid  13835  ghmmulg  13842  resghm  13846  invghm  13915  gsumfzmptfidmadd  13925  mgptopng  13941  srgisid  13998  ringidss  14041  ringcom  14043  opprsubgg  14096  unitgrp  14129  1rinv  14141  0unit  14142  rhmdvdsr  14188  lringuplu  14209  subrngpropd  14229  subrgpropd  14266  lmod0vs  14334  lmodvsmmulgdi  14336  lmodvneg1  14343  lmodcom  14346  lmodsubvs  14356  lmodsubdir  14358  lmodpropd  14362  lspsnsub  14434  lspsneq0b  14440  lsppropd  14445  rlmscabas  14473  lidlbas  14491  zringmulg  14611  restopnb  14904  txcnmpt  14996  cnmpt1t  15008  blhalf  15131  xmspropd  15200  mspropd  15201  mpomulcn  15289  ivthreinc  15368  limcimolemlt  15387  dvfre  15433  dveflem  15449  dvef  15450  ply1termlem  15465  plymullem1  15471  sin2kpi  15534  cos2kpi  15535  sin2pim  15536  cos2pim  15537  ptolemy  15547  sincosq2sgn  15550  sincosq3sgn  15551  sincosq4sgn  15552  sinq12gt0  15553  tangtx  15561  sincosq1eq  15562  abssinper  15569  sinkpi  15570  relogeftb  15588  relogoprlem  15591  relogexp  15595  mpodvdsmulf1o  15713  mersenne  15720  perfectlem1  15722  perfectlem2  15723  perfect  15724  lgsval2lem  15738  lgsdir2lem4  15759  lgsdirprm  15762  lgsdilem2  15764  gausslemma2dlem7  15796  lgseisenlem4  15801  lgsquadlem1  15805  lgsquadlem2  15806  lgsquad2lem1  15809  lgsquad2lem2  15810  2sqlem4  15846  2sqlem6  15848  2sqlem8  15851  clwwlknonel  16282  peano3nninf  16609  nninfsel  16619  nninffeq  16622  isomninnlem  16634  cvgcmp2nlemabs  16636  trilpolemlt1  16645  trirec0xor  16649  ismkvnnlem  16656  gfsum0  16682