Theorem eqtr3d 2269

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 2240	. 2 |- ( ph -> B = A )
3		eqtr3d.2	. 2 |- ( ph -> A = C )
4	2, 3	eqtrd 2267	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 2216

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

This theorem is referenced by:  3eqtr3d  2275  3eqtr3rd  2276  3eqtr3a  2291  opth  4358  eusvnf  4579  f00  5564  f1imacnv  5636  foimacnv  5637  f1ococnv1  5648  funfvdm  5745  fvmptdf  5770  fndmdif  5788  funopsn  5865  acexmidlemph  6051  acexmidlemab  6052  ovmpodf  6193  fvmpopr2d  6198  oprssov  6204  tfrlemisucaccv  6569  tfr1onlemsucaccv  6585  tfrcllemsucaccv  6598  oav2  6709  omv2  6711  fnsnsplitdc  6751  ecopovtrn  6879  ecopovtrng  6882  map0b  6934  en1  7052  ssenen  7118  fidifsnen  7138  dif1en  7149  undifdc  7197  fidcenumlemr  7238  ordiso2  7339  nninfninc  7427  nnnninfeq2  7433  nninfisollemne  7435  finomni  7444  exmidomni  7446  fodjum  7450  exmidaclem  7528  distrnqg  7718  1qec  7719  prarloclemarch2  7750  nnnq0lem1  7777  nqpnq0nq  7784  distrnq0  7790  prarloclemlt  7824  prmuloclemcalc  7896  ltaprg  7950  prplnqu  7951  recexprlem1ssl  7964  recexprlem1ssu  7965  ltmprr  7973  cauappcvgprlemopl  7977  caucvgprlemopl  8000  caucvgprprlemopl  8028  caucvgprprlemexb  8038  prsrlem1  8073  ltsosr  8095  mulgt0sr  8109  recidpipr  8187  recriota  8221  nntopi  8225  axcaucvglemres  8230  addlid  8428  readdcan  8429  muladd11r  8445  add32r  8449  cnegexlem2  8465  cnegex  8467  pncan2  8496  addsubass  8499  subadd23  8501  addsub12  8502  subid  8508  subid1  8509  npncan  8510  nppcan3  8513  subsub  8519  nppcan2  8520  nnncan2  8526  npncan3  8527  pnpcan  8528  negdi  8546  mvlraddd  8653  mvlladdd  8654  pnpncand  8664  subdi  8675  mulsub  8691  mulsub2  8692  eqord1  8774  recexap  8944  div32ap  8983  divsubdirap  8999  divmuldivap  9003  divdivdivap  9004  divmuleqap  9008  divcanap6  9010  dmdcanap  9013  divsubdivap  9019  div2negap  9026  div2subap  9128  mvllmulapd  9133  prodgt0gt0  9142  cju  9252  zneo  9697  infrenegsupex  9944  qreccl  9992  mul2lt0rlt0  10110  xnpcan  10224  fzosn  10572  modqid  10735  modqm1p1mod0  10761  modqltm1p1mod  10762  modqmul1  10763  modaddmodup  10773  modaddmodlo  10774  modqsubdir  10779  iseqf1olemkle  10883  iseqf1olemklt  10884  seq3f1olemstep  10900  seq3f1oleml  10902  seqf1oglem2  10906  seqfeq3  10915  seq3distr  10918  expineg2  10934  expm1t  10953  expadd  10967  expaddzaplem  10968  expmulzap  10971  sqsubswap  10985  subsq2  11033  binom2sub  11039  binom3  11043  resq01  11044  facndiv  11126  bcval5  11150  bcn2p1  11158  bcnm1  11160  hashpwfi  11218  hashfibclem  11231  pfxccatpfx2  11454  2shfti  11541  shftcan2  11545  reim0  11571  imval2  11604  cjreim2  11614  cjdivap  11619  cnrecnv  11620  rennim  11712  resqrexlemnm  11728  remsqsqrt  11742  sqrtdiv  11752  sqrtmsq  11755  sqabsadd  11765  sqabssub  11766  absreim  11778  absdivap  11780  absnid  11783  sqabs  11792  abslt  11798  absle  11799  recvalap  11807  abssub  11811  maxabslemlub  11917  infxrnegsupex  11973  mulcn2  12022  reccn2ap  12023  cjcn2  12026  summodclem3  12091  summodclem2a  12092  summodc  12094  zsumdc  12095  fsum3  12098  fisumss  12103  fsumcl2lem  12109  fsumm1  12127  fsum1p  12129  isummulc2  12137  telfsumo  12177  binomlem  12194  bcxmas  12200  arisum  12209  trireciplem  12211  trirecip  12212  geolim2  12223  georeclim  12224  cvgratnnlemfm  12240  cvgratz  12243  mertenslemi1  12246  clim2divap  12251  prodmodclem3  12286  prodmodclem2a  12287  zproddc  12290  fprodseq  12294  fprodssdc  12301  fprod1p  12310  efcan  12387  efexp  12393  efzval  12394  efgt0  12395  eftlub  12401  efltim  12409  resinval  12426  recosval  12427  cosmul  12456  cos2t  12461  cos2tsin  12462  cos01bnd  12469  cos12dec  12479  eirraplem  12488  muldvds1  12527  dvdsexp  12572  oexpneg  12588  divalglemqt  12630  divalglemeunn  12632  divalglemeuneg  12634  divalgmod  12638  flodddiv4t2lthalf  12650  bitsmod  12667  bitsinv1lem  12672  gcdid0  12701  gcdaddm  12705  dvdsgcdidd  12715  rpmulgcd  12747  sqgcd  12750  algcvg  12770  eucalgcvga  12780  eucalg  12781  dvdslcm  12791  lcmeq0  12793  lcmgcd  12800  qredeu  12819  sqnprm  12858  divgcdodd  12865  sqrt2irrlem  12883  sqpweven  12897  2sqpwodd  12898  divnumden  12918  hashdvds  12943  phimullem  12947  eulerthlemrprm  12951  eulerthlemth  12954  odzdvds  12968  pythagtriplem3  12990  pythagtriplem4  12991  pythagtriplem14  13000  pythagtriplem19  13005  pcpremul  13016  pceulem  13017  pcqdiv  13030  pcaddlem  13062  fldivp1  13071  1arithlem4  13089  4sqlem10  13110  mul4sqlem  13116  4sqlem11  13124  4sqlem15  13128  4sqlem16  13129  4sqlem17  13130  ballotfilemfc0  13176  ballotfilemfcc  13177  ballotfilemic  13194  ballotfilem1c  13195  ballotfilemfrceq  13216  ballotfilemrinv0  13220  ennnfonelemhf1o  13248  strslssd  13343  ressbas2d  13365  ressinbasd  13371  topnidg  13549  lidrideqd  13644  grpidd  13646  grprida  13650  gsumress  13658  ismndd  13698  grpidd2  13796  grpinvid1  13807  grpinvid2  13808  grppnpcan2  13849  grpnpncan  13850  dfgrp3mlem  13853  grpsubpropd2  13860  mhmid  13868  mhmmnd  13869  mulgsubcl  13889  mulgneg  13893  mulgaddcomlem  13898  mulginvinv  13901  mulgdirlem  13906  mulgdir  13907  mulgass  13912  mulgmodid  13914  grpissubg  13947  eqgcpbl  13981  ghmid  14002  ghmmulg  14009  resghm  14013  invghm  14082  gsumfzmptfidmadd  14092  gfsum0  14104  mgptopng  14168  srgisid  14229  ringidss  14272  ringcom  14274  opprsubgg  14328  unitgrp  14361  1rinv  14373  0unit  14374  rhmdvdsr  14420  lringuplu  14441  subrngpropd  14462  subrgpropd  14499  lmod0vs  14595  lmodvsmmulgdi  14597  lmodvneg1  14604  lmodcom  14607  lmodsubvs  14617  lmodsubdir  14619  lmodpropd  14623  lspsnsub  14695  lspsneq0b  14701  lsppropd  14706  rlmscabas  14734  lidlbas  14752  zringmulg  14872  restopnb  15172  txcnmpt  15264  cnmpt1t  15276  blhalf  15399  xmspropd  15468  mspropd  15469  mpomulcn  15557  ivthreinc  15636  limcimolemlt  15655  dvfre  15701  dveflem  15717  dvef  15718  ply1termlem  15733  plymullem1  15739  sin2kpi  15802  cos2kpi  15803  sin2pim  15804  cos2pim  15805  ptolemy  15815  sincosq2sgn  15818  sincosq3sgn  15819  sincosq4sgn  15820  sinq12gt0  15821  tangtx  15829  sincosq1eq  15830  abssinper  15837  sinkpi  15838  relogeftb  15856  relogoprlem  15859  relogexp  15863  pellexlem1  15971  mpodvdsmulf1o  15984  mersenne  15991  perfectlem1  15993  perfectlem2  15994  perfect  15995  lgsval2lem  16009  lgsdir2lem4  16030  lgsdirprm  16033  lgsdilem2  16035  gausslemma2dlem7  16067  lgseisenlem4  16072  lgsquadlem1  16076  lgsquadlem2  16077  lgsquad2lem1  16080  lgsquad2lem2  16081  2sqlem4  16117  2sqlem6  16119  2sqlem8  16122  clwwlknonel  16553  eupth2fi  16600  peano3nninf  16911  nninfsel  16921  nninffeq  16924  isomninnlem  16940  cvgcmp2nlemabs  16942  trilpolemlt1  16951  trirec0xor  16955  qdiff  16959  ismkvnnlem  16963