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 1398

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575  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  4335  eusvnf  4556  f00  5537  f1imacnv  5609  foimacnv  5610  f1ococnv1  5621  funfvdm  5718  fvmptdf  5743  fndmdif  5761  funopsn  5838  acexmidlemph  6021  acexmidlemab  6022  ovmpodf  6163  fvmpopr2d  6168  oprssov  6174  tfrlemisucaccv  6534  tfr1onlemsucaccv  6550  tfrcllemsucaccv  6563  oav2  6674  omv2  6676  fnsnsplitdc  6716  ecopovtrn  6844  ecopovtrng  6847  map0b  6899  en1  7016  ssenen  7080  fidifsnen  7100  dif1en  7111  undifdc  7159  fidcenumlemr  7197  ordiso2  7277  nninfninc  7365  nnnninfeq2  7371  nninfisollemne  7373  finomni  7382  exmidomni  7384  fodjum  7388  exmidaclem  7466  distrnqg  7650  1qec  7651  prarloclemarch2  7682  nnnq0lem1  7709  nqpnq0nq  7716  distrnq0  7722  prarloclemlt  7756  prmuloclemcalc  7828  ltaprg  7882  prplnqu  7883  recexprlem1ssl  7896  recexprlem1ssu  7897  ltmprr  7905  cauappcvgprlemopl  7909  caucvgprlemopl  7932  caucvgprprlemopl  7960  caucvgprprlemexb  7970  prsrlem1  8005  ltsosr  8027  mulgt0sr  8041  recidpipr  8119  recriota  8153  nntopi  8157  axcaucvglemres  8162  addlid  8360  readdcan  8361  muladd11r  8377  add32r  8381  cnegexlem2  8397  cnegex  8399  pncan2  8428  addsubass  8431  subadd23  8433  addsub12  8434  subid  8440  subid1  8441  npncan  8442  nppcan3  8445  subsub  8451  nppcan2  8452  nnncan2  8458  npncan3  8459  pnpcan  8460  negdi  8478  mvlraddd  8585  mvlladdd  8586  pnpncand  8596  subdi  8606  mulsub  8622  mulsub2  8623  eqord1  8705  recexap  8875  div32ap  8914  divsubdirap  8930  divmuldivap  8934  divdivdivap  8935  divmuleqap  8939  divcanap6  8941  dmdcanap  8944  divsubdivap  8950  div2negap  8957  div2subap  9059  mvllmulapd  9064  prodgt0gt0  9073  cju  9183  zneo  9625  infrenegsupex  9872  qreccl  9920  mul2lt0rlt0  10038  xnpcan  10151  fzosn  10496  modqid  10657  modqm1p1mod0  10683  modqltm1p1mod  10684  modqmul1  10685  modaddmodup  10695  modaddmodlo  10696  modqsubdir  10701  iseqf1olemkle  10805  iseqf1olemklt  10806  seq3f1olemstep  10822  seq3f1oleml  10824  seqf1oglem2  10828  seqfeq3  10837  seq3distr  10840  expineg2  10856  expm1t  10875  expadd  10889  expaddzaplem  10890  expmulzap  10893  sqsubswap  10907  subsq2  10955  binom2sub  10961  binom3  10965  facndiv  11047  bcval5  11071  bcn2p1  11078  bcnm1  11080  pfxccatpfx2  11367  2shfti  11454  shftcan2  11458  reim0  11484  imval2  11517  cjreim2  11527  cjdivap  11532  cnrecnv  11533  rennim  11625  resqrexlemnm  11641  remsqsqrt  11655  sqrtdiv  11665  sqrtmsq  11668  sqabsadd  11678  sqabssub  11679  absreim  11691  absdivap  11693  absnid  11696  sqabs  11705  abslt  11711  absle  11712  recvalap  11720  abssub  11724  maxabslemlub  11830  infxrnegsupex  11886  mulcn2  11935  reccn2ap  11936  cjcn2  11939  summodclem3  12004  summodclem2a  12005  summodc  12007  zsumdc  12008  fsum3  12011  fisumss  12016  fsumcl2lem  12022  fsumm1  12040  fsum1p  12042  isummulc2  12050  telfsumo  12090  binomlem  12107  bcxmas  12113  arisum  12122  trireciplem  12124  trirecip  12125  geolim2  12136  georeclim  12137  cvgratnnlemfm  12153  cvgratz  12156  mertenslemi1  12159  clim2divap  12164  prodmodclem3  12199  prodmodclem2a  12200  zproddc  12203  fprodseq  12207  fprodssdc  12214  fprod1p  12223  efcan  12300  efexp  12306  efzval  12307  efgt0  12308  eftlub  12314  efltim  12322  resinval  12339  recosval  12340  cosmul  12369  cos2t  12374  cos2tsin  12375  cos01bnd  12382  cos12dec  12392  eirraplem  12401  muldvds1  12440  dvdsexp  12485  oexpneg  12501  divalglemqt  12543  divalglemeunn  12545  divalglemeuneg  12547  divalgmod  12551  flodddiv4t2lthalf  12563  bitsmod  12580  bitsinv1lem  12585  gcdid0  12614  gcdaddm  12618  dvdsgcdidd  12628  rpmulgcd  12660  sqgcd  12663  algcvg  12683  eucalgcvga  12693  eucalg  12694  dvdslcm  12704  lcmeq0  12706  lcmgcd  12713  qredeu  12732  sqnprm  12771  divgcdodd  12778  sqrt2irrlem  12796  sqpweven  12810  2sqpwodd  12811  divnumden  12831  hashdvds  12856  phimullem  12860  eulerthlemrprm  12864  eulerthlemth  12867  odzdvds  12881  pythagtriplem3  12903  pythagtriplem4  12904  pythagtriplem14  12913  pythagtriplem19  12918  pcpremul  12929  pceulem  12930  pcqdiv  12943  pcaddlem  12975  fldivp1  12984  1arithlem4  13002  4sqlem10  13023  mul4sqlem  13029  4sqlem11  13037  4sqlem15  13041  4sqlem16  13042  4sqlem17  13043  ennnfonelemhf1o  13097  strslssd  13192  ressbas2d  13214  ressinbasd  13220  topnidg  13398  lidrideqd  13527  grpidd  13529  grprida  13533  gsumress  13541  ismndd  13583  grpidd2  13687  grpinvid1  13698  grpinvid2  13699  grppnpcan2  13740  grpnpncan  13741  dfgrp3mlem  13744  grpsubpropd2  13751  mhmid  13765  mhmmnd  13766  mulgsubcl  13786  mulgneg  13790  mulgaddcomlem  13795  mulginvinv  13798  mulgdirlem  13803  mulgdir  13804  mulgass  13809  mulgmodid  13811  grpissubg  13844  eqgcpbl  13878  ghmid  13899  ghmmulg  13906  resghm  13910  invghm  13979  gsumfzmptfidmadd  13989  mgptopng  14006  srgisid  14063  ringidss  14106  ringcom  14108  opprsubgg  14161  unitgrp  14194  1rinv  14206  0unit  14207  rhmdvdsr  14253  lringuplu  14274  subrngpropd  14294  subrgpropd  14331  lmod0vs  14400  lmodvsmmulgdi  14402  lmodvneg1  14409  lmodcom  14412  lmodsubvs  14422  lmodsubdir  14424  lmodpropd  14428  lspsnsub  14500  lspsneq0b  14506  lsppropd  14511  rlmscabas  14539  lidlbas  14557  zringmulg  14677  restopnb  14975  txcnmpt  15067  cnmpt1t  15079  blhalf  15202  xmspropd  15271  mspropd  15272  mpomulcn  15360  ivthreinc  15439  limcimolemlt  15458  dvfre  15504  dveflem  15520  dvef  15521  ply1termlem  15536  plymullem1  15542  sin2kpi  15605  cos2kpi  15606  sin2pim  15607  cos2pim  15608  ptolemy  15618  sincosq2sgn  15621  sincosq3sgn  15622  sincosq4sgn  15623  sinq12gt0  15624  tangtx  15632  sincosq1eq  15633  abssinper  15640  sinkpi  15641  relogeftb  15659  relogoprlem  15662  relogexp  15666  pellexlem1  15774  mpodvdsmulf1o  15787  mersenne  15794  perfectlem1  15796  perfectlem2  15797  perfect  15798  lgsval2lem  15812  lgsdir2lem4  15833  lgsdirprm  15836  lgsdilem2  15838  gausslemma2dlem7  15870  lgseisenlem4  15875  lgsquadlem1  15879  lgsquadlem2  15880  lgsquad2lem1  15883  lgsquad2lem2  15884  2sqlem4  15920  2sqlem6  15922  2sqlem8  15925  clwwlknonel  16356  eupth2fi  16403  peano3nninf  16716  nninfsel  16726  nninffeq  16729  isomninnlem  16745  cvgcmp2nlemabs  16747  trilpolemlt1  16756  trirec0xor  16760  qdiff  16764  ismkvnnlem  16768  gfsum0  16794