Theorem eqtr3d 2273

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

This proof depends on syntax axioms:   -> wi 4   = wceq 1402

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231

This theorem is used by:  3eqtr3d  2279  3eqtr3rd  2280  3eqtr3a  2295  opth  4379  eusvnf  4601  f00  5587  f1imacnv  5659  foimacnv  5660  f1ococnv1  5671  funfvdm  5769  fvmptdf  5796  fndmdif  5817  funopsn  5894  acexmidlemph  6081  acexmidlemab  6082  ovmpodf  6223  fvmpopr2d  6228  oprssov  6234  tfrlemisucaccv  6601  tfr1onlemsucaccv  6617  tfrcllemsucaccv  6630  oav2  6741  omv2  6743  fnsnsplitdc  6783  ecopovtrn  6911  ecopovtrng  6914  map0b  6973  en1  7092  ssenen  7158  fidifsnen  7178  dif1en  7189  undifdc  7237  fidcenumlemr  7279  ordiso2  7381  nninfninc  7469  nnnninfeq2  7475  nninfisollemne  7477  finomni  7486  exmidomni  7488  fodjum  7492  exmidaclem  7570  distrnqg  7760  1qec  7761  prarloclemarch2  7792  nnnq0lem1  7819  nqpnq0nq  7826  distrnq0  7832  prarloclemlt  7866  prmuloclemcalc  7938  ltaprg  7992  prplnqu  7993  recexprlem1ssl  8006  recexprlem1ssu  8007  ltmprr  8015  cauappcvgprlemopl  8019  caucvgprlemopl  8042  caucvgprprlemopl  8070  caucvgprprlemexb  8080  prsrlem1  8115  ltsosr  8137  mulgt0sr  8151  recidpipr  8229  recriota  8263  nntopi  8267  axcaucvglemres  8272  addlid  8472  readdcan  8473  muladd11r  8489  add32r  8493  cnegexlem2  8509  cnegex  8511  pncan2  8540  addsubass  8543  subadd23  8545  addsub12  8546  subid  8552  subid1  8553  npncan  8554  nppcan3  8557  subsub  8563  nppcan2  8564  nnncan2  8570  npncan3  8571  pnpcan  8572  negdi  8590  mvlraddd  8697  mvlladdd  8698  pnpncand  8708  subdi  8719  mulsub  8735  mulsub2  8736  eqord1  8818  recexap  8989  div32ap  9030  divsubdirap  9046  divmuldivap  9050  divdivdivap  9051  divmuleqap  9055  divcanap6  9057  dmdcanap  9060  divsubdivap  9066  div2negap  9073  div2subap  9175  mvllmulapd  9180  prodgt0gt0  9189  cju  9299  zneo  9757  infrenegsupex  10009  qreccl  10057  mul2lt0rlt0  10176  xnpcan  10290  fzosn  10639  modqid  10806  modqm1p1mod0  10832  modqltm1p1mod  10833  modqmul1  10834  modaddmodup  10844  modaddmodlo  10845  modqsubdir  10850  iseqf1olemkle  10954  iseqf1olemklt  10955  seq3f1olemstep  10971  seq3f1oleml  10973  seqf1oglem2  10977  seqfeq3  10986  seq3distr  10989  expineg2  11005  expm1t  11024  expadd  11038  expaddzaplem  11039  expmulzap  11042  sqsubswap  11056  subsq2  11104  binom2sub  11110  binom3  11114  resq01  11115  facndiv  11198  bcval5  11222  bcn2p1  11230  bcnm1  11232  hashpwfi  11290  hashfibclem  11303  pfxccatpfx2  11530  2shfti  11617  shftcan2  11621  reim0  11647  imval2  11680  cjreim2  11691  cjdivap  11696  cnrecnv  11697  rennim  11789  resqrexlemnm  11805  remsqsqrt  11819  sqrtdiv  11829  sqrtmsq  11832  sqabsadd  11842  sqabssub  11843  absreim  11855  absdivap  11857  absnid  11860  sqabs  11870  abslt  11876  absle  11877  recvalap  11885  abssub  11889  maxabslemlub  11995  infxrnegsupex  12053  mulcn2  12102  reccn2ap  12103  cjcn2  12106  summodclem3  12171  summodclem2a  12172  summodc  12174  zsumdc  12175  fsum3  12178  fisumss  12183  fsumcl2lem  12189  fsumm1  12207  fsum1p  12209  isummulc2  12217  telfsumo  12257  binomlem  12274  bcxmas  12280  arisum  12289  trireciplem  12291  trirecip  12292  geolim2  12303  georeclim  12304  cvgratnnlemfm  12320  cvgratz  12323  mertenslemi1  12326  clim2divap  12331  prodmodclem3  12366  prodmodclem2a  12367  zproddc  12370  fprodseq  12374  fprodssdc  12381  fprod1p  12390  efcan  12467  efexp  12473  efzval  12474  efgt0  12475  eftlub  12481  efltim  12489  resinval  12506  recosval  12507  cosmul  12536  cos2t  12541  cos2tsin  12542  cos01bnd  12549  cos12dec  12559  eirraplem  12568  muldvds1  12607  dvdsexp  12652  oexpneg  12668  divalglemqt  12710  divalglemeunn  12712  divalglemeuneg  12714  divalgmod  12718  flodddiv4t2lthalf  12730  bitsmod  12747  bitsinv1lem  12752  gcdid0  12781  gcdaddm  12785  dvdsgcdidd  12795  rpmulgcd  12827  sqgcd  12830  algcvg  12850  eucalgcvga  12860  eucalg  12861  dvdslcm  12871  lcmeq0  12873  lcmgcd  12880  qredeu  12899  sqnprm  12939  divgcdodd  12946  sqrt2irrlem  12964  sqpweven  12979  2sqpwodd  12980  divnumden  13000  hashdvds  13027  phimullem  13031  eulerthlemrprm  13035  eulerthlemth  13038  odzdvds  13052  pythagtriplem3  13074  pythagtriplem4  13075  pythagtriplem14  13084  pythagtriplem19  13089  pcpremul  13100  pceulem  13101  pcqdiv  13114  pcaddlem  13146  fldivp1  13155  1arithlem4  13173  4sqlem10  13194  mul4sqlem  13200  4sqlem11  13208  4sqlem15  13212  4sqlem16  13213  4sqlem17  13214  ballotfilemfc0  13289  ballotfilemfcc  13290  ballotfilemic  13307  ballotfilem1c  13308  ballotfilemfrceq  13329  ballotfilemrinv0  13333  ennnfonelemhf1o  13361  strslssd  13456  ressbas2d  13480  ressinbasd  13486  topnidg  13664  lidrideqd  13759  grpidd  13761  grprida  13765  gzsumress  13770  ismndd  13808  grpidd2  13904  grpinvid1  13915  grpinvid2  13916  grppnpcan2  13957  grpnpncan  13958  dfgrp3mlem  13961  grpsubpropd2  13968  mhmid  13976  mhmmnd  13977  mulgsubcl  13997  mulgneg  14001  mulgaddcomlem  14006  mulginvinv  14009  mulgdirlem  14014  mulgdir  14015  mulgass  14020  mulgmodid  14022  grpissubg  14055  eqgcpbl  14089  ghmid  14110  ghmmulg  14117  resghm  14121  cntrsubgnsg  14174  invghm  14222  gsum0cmn  14243  gsumresfi  14262  gsum2dfilem2  14271  mgptopng  14334  srgisid  14396  ringidss  14440  ringcom  14442  opprsubgg  14498  unitgrp  14531  1rinv  14543  0unit  14544  rhmdvdsr  14590  lringuplu  14611  subrngpropd  14632  subrgpropd  14669  lmod0vs  14766  lmodvsmmulgdi  14768  lmodvneg1  14775  lmodcom  14778  lmodsubvs  14788  lmodsubdir  14790  lmodpropd  14794  lspsnsub  14866  lspsneq0b  14872  lsppropd  14877  rlmscabas  14905  lidlbas  14923  zringmulg  15041  mvrclfi  15226  restopnb  15424  txcnmpt  15516  cnmpt1t  15528  blhalf  15651  xmspropd  15720  mspropd  15721  mpomulcn  15809  ivthreinc  15888  limcimolemlt  15907  dvfre  15953  dveflem  15969  dvef  15970  ply1termlem  15985  plymullem1  15991  sin2kpi  16055  cos2kpi  16056  sin2pim  16057  cos2pim  16058  ptolemy  16068  sincosq2sgn  16071  sincosq3sgn  16072  sincosq4sgn  16073  sinq12gt0  16074  tangtx  16082  sincosq1eq  16083  abssinper  16090  sinkpi  16091  sineq0re  16093  root1idef  16101  relogeftb  16111  relogoprlem  16115  relogexp  16119  rpcxpmul2z  16165  log2tlbndlog2  16237  birthdaylem2  16243  birthdaylem3  16244  pellexlem1  16246  efchtqdvds  16282  ppiqp1le  16284  ppiqltx  16298  mpodvdsmulf1o  16301  ppiqub  16310  chtqub  16313  mersenne  16314  perfectlem1  16316  perfectlem2  16317  perfect  16318  bposlem6  16333  bposlem9  16336  lgsval2lem  16351  lgsdir2lem4  16372  lgsdirprm  16375  lgsdilem2  16377  gausslemma2dlem7  16409  lgseisenlem4  16414  lgsquadlem1  16418  lgsquadlem2  16419  lgsquad2lem1  16422  lgsquad2lem2  16423  2sqlem4  16459  2sqlem6  16461  2sqlem8  16464  clwwlknonel  16895  eupth2fi  16942  dichmul0orlem2  16976  dichmul0orlem3  16977  dichmul0orlem4  16978  peano3nninf  17273  nninfsel  17283  nninffeq  17286  isomninnlem  17302  cvgcmp2nlemabs  17304  trilpolemlt1  17314  trirec0xor  17318  qdiff  17322  ismkvnnlem  17326