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  4327  eusvnf  4548  f00  5525  f1imacnv  5597  foimacnv  5598  f1ococnv1  5609  funfvdm  5705  fvmptdf  5730  fndmdif  5748  funopsn  5825  acexmidlemph  6006  acexmidlemab  6007  ovmpodf  6148  fvmpopr2d  6153  oprssov  6159  tfrlemisucaccv  6486  tfr1onlemsucaccv  6502  tfrcllemsucaccv  6515  oav2  6626  omv2  6628  fnsnsplitdc  6668  ecopovtrn  6796  ecopovtrng  6799  map0b  6851  en1  6968  ssenen  7032  fidifsnen  7052  dif1en  7061  undifdc  7109  fidcenumlemr  7145  ordiso2  7225  nninfninc  7313  nnnninfeq2  7319  nninfisollemne  7321  finomni  7330  exmidomni  7332  fodjum  7336  exmidaclem  7413  distrnqg  7597  1qec  7598  prarloclemarch2  7629  nnnq0lem1  7656  nqpnq0nq  7663  distrnq0  7669  prarloclemlt  7703  prmuloclemcalc  7775  ltaprg  7829  prplnqu  7830  recexprlem1ssl  7843  recexprlem1ssu  7844  ltmprr  7852  cauappcvgprlemopl  7856  caucvgprlemopl  7879  caucvgprprlemopl  7907  caucvgprprlemexb  7917  prsrlem1  7952  ltsosr  7974  mulgt0sr  7988  recidpipr  8066  recriota  8100  nntopi  8104  axcaucvglemres  8109  addlid  8308  readdcan  8309  muladd11r  8325  add32r  8329  cnegexlem2  8345  cnegex  8347  pncan2  8376  addsubass  8379  subadd23  8381  addsub12  8382  subid  8388  subid1  8389  npncan  8390  nppcan3  8393  subsub  8399  nppcan2  8400  nnncan2  8406  npncan3  8407  pnpcan  8408  negdi  8426  mvlraddd  8533  mvlladdd  8534  pnpncand  8544  subdi  8554  mulsub  8570  mulsub2  8571  eqord1  8653  recexap  8823  div32ap  8862  divsubdirap  8878  divmuldivap  8882  divdivdivap  8883  divmuleqap  8887  divcanap6  8889  dmdcanap  8892  divsubdivap  8898  div2negap  8905  div2subap  9007  mvllmulapd  9012  prodgt0gt0  9021  cju  9131  zneo  9571  infrenegsupex  9818  qreccl  9866  mul2lt0rlt0  9984  xnpcan  10097  fzosn  10440  modqid  10601  modqm1p1mod0  10627  modqltm1p1mod  10628  modqmul1  10629  modaddmodup  10639  modaddmodlo  10640  modqsubdir  10645  iseqf1olemkle  10749  iseqf1olemklt  10750  seq3f1olemstep  10766  seq3f1oleml  10768  seqf1oglem2  10772  seqfeq3  10781  seq3distr  10784  expineg2  10800  expm1t  10819  expadd  10833  expaddzaplem  10834  expmulzap  10837  sqsubswap  10851  subsq2  10899  binom2sub  10905  binom3  10909  facndiv  10991  bcval5  11015  bcn2p1  11022  bcnm1  11024  pfxccatpfx2  11308  2shfti  11382  shftcan2  11386  reim0  11412  imval2  11445  cjreim2  11455  cjdivap  11460  cnrecnv  11461  rennim  11553  resqrexlemnm  11569  remsqsqrt  11583  sqrtdiv  11593  sqrtmsq  11596  sqabsadd  11606  sqabssub  11607  absreim  11619  absdivap  11621  absnid  11624  sqabs  11633  abslt  11639  absle  11640  recvalap  11648  abssub  11652  maxabslemlub  11758  infxrnegsupex  11814  mulcn2  11863  reccn2ap  11864  cjcn2  11867  summodclem3  11931  summodclem2a  11932  summodc  11934  zsumdc  11935  fsum3  11938  fisumss  11943  fsumcl2lem  11949  fsumm1  11967  fsum1p  11969  isummulc2  11977  telfsumo  12017  binomlem  12034  bcxmas  12040  arisum  12049  trireciplem  12051  trirecip  12052  geolim2  12063  georeclim  12064  cvgratnnlemfm  12080  cvgratz  12083  mertenslemi1  12086  clim2divap  12091  prodmodclem3  12126  prodmodclem2a  12127  zproddc  12130  fprodseq  12134  fprodssdc  12141  fprod1p  12150  efcan  12227  efexp  12233  efzval  12234  efgt0  12235  eftlub  12241  efltim  12249  resinval  12266  recosval  12267  cosmul  12296  cos2t  12301  cos2tsin  12302  cos01bnd  12309  cos12dec  12319  eirraplem  12328  muldvds1  12367  dvdsexp  12412  oexpneg  12428  divalglemqt  12470  divalglemeunn  12472  divalglemeuneg  12474  divalgmod  12478  flodddiv4t2lthalf  12490  bitsmod  12507  bitsinv1lem  12512  gcdid0  12541  gcdaddm  12545  dvdsgcdidd  12555  rpmulgcd  12587  sqgcd  12590  algcvg  12610  eucalgcvga  12620  eucalg  12621  dvdslcm  12631  lcmeq0  12633  lcmgcd  12640  qredeu  12659  sqnprm  12698  divgcdodd  12705  sqrt2irrlem  12723  sqpweven  12737  2sqpwodd  12738  divnumden  12758  hashdvds  12783  phimullem  12787  eulerthlemrprm  12791  eulerthlemth  12794  odzdvds  12808  pythagtriplem3  12830  pythagtriplem4  12831  pythagtriplem14  12840  pythagtriplem19  12845  pcpremul  12856  pceulem  12857  pcqdiv  12870  pcaddlem  12902  fldivp1  12911  1arithlem4  12929  4sqlem10  12950  mul4sqlem  12956  4sqlem11  12964  4sqlem15  12968  4sqlem16  12969  4sqlem17  12970  ennnfonelemhf1o  13024  strslssd  13119  ressbas2d  13141  ressinbasd  13147  topnidg  13325  lidrideqd  13454  grpidd  13456  grprida  13460  gsumress  13468  ismndd  13510  grpidd2  13614  grpinvid1  13625  grpinvid2  13626  grppnpcan2  13667  grpnpncan  13668  dfgrp3mlem  13671  grpsubpropd2  13678  mhmid  13692  mhmmnd  13693  mulgsubcl  13713  mulgneg  13717  mulgaddcomlem  13722  mulginvinv  13725  mulgdirlem  13730  mulgdir  13731  mulgass  13736  mulgmodid  13738  grpissubg  13771  eqgcpbl  13805  ghmid  13826  ghmmulg  13833  resghm  13837  invghm  13906  gsumfzmptfidmadd  13916  mgptopng  13932  srgisid  13989  ringidss  14032  ringcom  14034  opprsubgg  14087  unitgrp  14120  1rinv  14132  0unit  14133  rhmdvdsr  14179  lringuplu  14200  subrngpropd  14220  subrgpropd  14257  lmod0vs  14325  lmodvsmmulgdi  14327  lmodvneg1  14334  lmodcom  14337  lmodsubvs  14347  lmodsubdir  14349  lmodpropd  14353  lspsnsub  14425  lspsneq0b  14431  lsppropd  14436  rlmscabas  14464  lidlbas  14482  zringmulg  14602  restopnb  14895  txcnmpt  14987  cnmpt1t  14999  blhalf  15122  xmspropd  15191  mspropd  15192  mpomulcn  15280  ivthreinc  15359  limcimolemlt  15378  dvfre  15424  dveflem  15440  dvef  15441  ply1termlem  15456  plymullem1  15462  sin2kpi  15525  cos2kpi  15526  sin2pim  15527  cos2pim  15528  ptolemy  15538  sincosq2sgn  15541  sincosq3sgn  15542  sincosq4sgn  15543  sinq12gt0  15544  tangtx  15552  sincosq1eq  15553  abssinper  15560  sinkpi  15561  relogeftb  15579  relogoprlem  15582  relogexp  15586  mpodvdsmulf1o  15704  mersenne  15711  perfectlem1  15713  perfectlem2  15714  perfect  15715  lgsval2lem  15729  lgsdir2lem4  15750  lgsdirprm  15753  lgsdilem2  15755  gausslemma2dlem7  15787  lgseisenlem4  15792  lgsquadlem1  15796  lgsquadlem2  15797  lgsquad2lem1  15800  lgsquad2lem2  15801  2sqlem4  15837  2sqlem6  15839  2sqlem8  15842  clwwlknonel  16227  peano3nninf  16545  nninfsel  16555  nninffeq  16558  isomninnlem  16570  cvgcmp2nlemabs  16572  trilpolemlt1  16581  trirec0xor  16585  ismkvnnlem  16592