Theorem eqtr3d 2267

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 2238	. 2 |- ( ph -> B = A )
3		eqtr3d.2	. 2 |- ( ph -> A = C )
4	2, 3	eqtrd 2265	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 2214

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

This theorem is referenced by:  3eqtr3d  2273  3eqtr3rd  2274  3eqtr3a  2289  opth  4353  eusvnf  4574  f00  5559  f1imacnv  5631  foimacnv  5632  f1ococnv1  5643  funfvdm  5740  fvmptdf  5765  fndmdif  5783  funopsn  5860  acexmidlemph  6043  acexmidlemab  6044  ovmpodf  6185  fvmpopr2d  6190  oprssov  6196  tfrlemisucaccv  6556  tfr1onlemsucaccv  6572  tfrcllemsucaccv  6585  oav2  6696  omv2  6698  fnsnsplitdc  6738  ecopovtrn  6866  ecopovtrng  6869  map0b  6921  en1  7039  ssenen  7105  fidifsnen  7125  dif1en  7136  undifdc  7184  fidcenumlemr  7225  ordiso2  7326  nninfninc  7414  nnnninfeq2  7420  nninfisollemne  7422  finomni  7431  exmidomni  7433  fodjum  7437  exmidaclem  7515  distrnqg  7702  1qec  7703  prarloclemarch2  7734  nnnq0lem1  7761  nqpnq0nq  7768  distrnq0  7774  prarloclemlt  7808  prmuloclemcalc  7880  ltaprg  7934  prplnqu  7935  recexprlem1ssl  7948  recexprlem1ssu  7949  ltmprr  7957  cauappcvgprlemopl  7961  caucvgprlemopl  7984  caucvgprprlemopl  8012  caucvgprprlemexb  8022  prsrlem1  8057  ltsosr  8079  mulgt0sr  8093  recidpipr  8171  recriota  8205  nntopi  8209  axcaucvglemres  8214  addlid  8412  readdcan  8413  muladd11r  8429  add32r  8433  cnegexlem2  8449  cnegex  8451  pncan2  8480  addsubass  8483  subadd23  8485  addsub12  8486  subid  8492  subid1  8493  npncan  8494  nppcan3  8497  subsub  8503  nppcan2  8504  nnncan2  8510  npncan3  8511  pnpcan  8512  negdi  8530  mvlraddd  8637  mvlladdd  8638  pnpncand  8648  subdi  8658  mulsub  8674  mulsub2  8675  eqord1  8757  recexap  8927  div32ap  8966  divsubdirap  8982  divmuldivap  8986  divdivdivap  8987  divmuleqap  8991  divcanap6  8993  dmdcanap  8996  divsubdivap  9002  div2negap  9009  div2subap  9111  mvllmulapd  9116  prodgt0gt0  9125  cju  9235  zneo  9679  infrenegsupex  9926  qreccl  9974  mul2lt0rlt0  10092  xnpcan  10205  fzosn  10550  modqid  10711  modqm1p1mod0  10737  modqltm1p1mod  10738  modqmul1  10739  modaddmodup  10749  modaddmodlo  10750  modqsubdir  10755  iseqf1olemkle  10859  iseqf1olemklt  10860  seq3f1olemstep  10876  seq3f1oleml  10878  seqf1oglem2  10882  seqfeq3  10891  seq3distr  10894  expineg2  10910  expm1t  10929  expadd  10943  expaddzaplem  10944  expmulzap  10947  sqsubswap  10961  subsq2  11009  binom2sub  11015  binom3  11019  facndiv  11101  bcval5  11125  bcn2p1  11133  bcnm1  11135  hashpwfi  11193  hashfibclem  11206  pfxccatpfx2  11429  2shfti  11516  shftcan2  11520  reim0  11546  imval2  11579  cjreim2  11589  cjdivap  11594  cnrecnv  11595  rennim  11687  resqrexlemnm  11703  remsqsqrt  11717  sqrtdiv  11727  sqrtmsq  11730  sqabsadd  11740  sqabssub  11741  absreim  11753  absdivap  11755  absnid  11758  sqabs  11767  abslt  11773  absle  11774  recvalap  11782  abssub  11786  maxabslemlub  11892  infxrnegsupex  11948  mulcn2  11997  reccn2ap  11998  cjcn2  12001  summodclem3  12066  summodclem2a  12067  summodc  12069  zsumdc  12070  fsum3  12073  fisumss  12078  fsumcl2lem  12084  fsumm1  12102  fsum1p  12104  isummulc2  12112  telfsumo  12152  binomlem  12169  bcxmas  12175  arisum  12184  trireciplem  12186  trirecip  12187  geolim2  12198  georeclim  12199  cvgratnnlemfm  12215  cvgratz  12218  mertenslemi1  12221  clim2divap  12226  prodmodclem3  12261  prodmodclem2a  12262  zproddc  12265  fprodseq  12269  fprodssdc  12276  fprod1p  12285  efcan  12362  efexp  12368  efzval  12369  efgt0  12370  eftlub  12376  efltim  12384  resinval  12401  recosval  12402  cosmul  12431  cos2t  12436  cos2tsin  12437  cos01bnd  12444  cos12dec  12454  eirraplem  12463  muldvds1  12502  dvdsexp  12547  oexpneg  12563  divalglemqt  12605  divalglemeunn  12607  divalglemeuneg  12609  divalgmod  12613  flodddiv4t2lthalf  12625  bitsmod  12642  bitsinv1lem  12647  gcdid0  12676  gcdaddm  12680  dvdsgcdidd  12690  rpmulgcd  12722  sqgcd  12725  algcvg  12745  eucalgcvga  12755  eucalg  12756  dvdslcm  12766  lcmeq0  12768  lcmgcd  12775  qredeu  12794  sqnprm  12833  divgcdodd  12840  sqrt2irrlem  12858  sqpweven  12872  2sqpwodd  12873  divnumden  12893  hashdvds  12918  phimullem  12922  eulerthlemrprm  12926  eulerthlemth  12929  odzdvds  12943  pythagtriplem3  12965  pythagtriplem4  12966  pythagtriplem14  12975  pythagtriplem19  12980  pcpremul  12991  pceulem  12992  pcqdiv  13005  pcaddlem  13037  fldivp1  13046  1arithlem4  13064  4sqlem10  13085  mul4sqlem  13091  4sqlem11  13099  4sqlem15  13103  4sqlem16  13104  4sqlem17  13105  ennnfonelemhf1o  13164  strslssd  13259  ressbas2d  13281  ressinbasd  13287  topnidg  13465  lidrideqd  13594  grpidd  13596  grprida  13600  gsumress  13608  ismndd  13650  grpidd2  13754  grpinvid1  13765  grpinvid2  13766  grppnpcan2  13807  grpnpncan  13808  dfgrp3mlem  13811  grpsubpropd2  13818  mhmid  13832  mhmmnd  13833  mulgsubcl  13853  mulgneg  13857  mulgaddcomlem  13862  mulginvinv  13865  mulgdirlem  13870  mulgdir  13871  mulgass  13876  mulgmodid  13878  grpissubg  13911  eqgcpbl  13945  ghmid  13966  ghmmulg  13973  resghm  13977  invghm  14046  gsumfzmptfidmadd  14056  mgptopng  14073  srgisid  14130  ringidss  14173  ringcom  14175  opprsubgg  14228  unitgrp  14261  1rinv  14273  0unit  14274  rhmdvdsr  14320  lringuplu  14341  subrngpropd  14361  subrgpropd  14398  lmod0vs  14469  lmodvsmmulgdi  14471  lmodvneg1  14478  lmodcom  14481  lmodsubvs  14491  lmodsubdir  14493  lmodpropd  14497  lspsnsub  14569  lspsneq0b  14575  lsppropd  14580  rlmscabas  14608  lidlbas  14626  zringmulg  14746  restopnb  15046  txcnmpt  15138  cnmpt1t  15150  blhalf  15273  xmspropd  15342  mspropd  15343  mpomulcn  15431  ivthreinc  15510  limcimolemlt  15529  dvfre  15575  dveflem  15591  dvef  15592  ply1termlem  15607  plymullem1  15613  sin2kpi  15676  cos2kpi  15677  sin2pim  15678  cos2pim  15679  ptolemy  15689  sincosq2sgn  15692  sincosq3sgn  15693  sincosq4sgn  15694  sinq12gt0  15695  tangtx  15703  sincosq1eq  15704  abssinper  15711  sinkpi  15712  relogeftb  15730  relogoprlem  15733  relogexp  15737  pellexlem1  15845  mpodvdsmulf1o  15858  mersenne  15865  perfectlem1  15867  perfectlem2  15868  perfect  15869  lgsval2lem  15883  lgsdir2lem4  15904  lgsdirprm  15907  lgsdilem2  15909  gausslemma2dlem7  15941  lgseisenlem4  15946  lgsquadlem1  15950  lgsquadlem2  15951  lgsquad2lem1  15954  lgsquad2lem2  15955  2sqlem4  15991  2sqlem6  15993  2sqlem8  15996  clwwlknonel  16427  eupth2fi  16474  peano3nninf  16785  nninfsel  16795  nninffeq  16798  isomninnlem  16814  cvgcmp2nlemabs  16816  trilpolemlt1  16825  trirec0xor  16829  qdiff  16833  ismkvnnlem  16837  gfsum0  16864