Theorem eqtr3d 2239

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

Syntax hints:   -> wi 4   = wceq 1372

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 1469  ax-gen 1471  ax-4 1532  ax-17 1548  ax-ext 2186

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

This theorem is referenced by:  3eqtr3d  2245  3eqtr3rd  2246  3eqtr3a  2261  opth  4280  eusvnf  4499  f00  5466  f1imacnv  5538  foimacnv  5539  f1ococnv1  5550  funfvdm  5641  fvmptdf  5666  fndmdif  5684  funopsn  5761  acexmidlemph  5936  acexmidlemab  5937  ovmpodf  6076  fvmpopr2d  6081  oprssov  6087  tfrlemisucaccv  6410  tfr1onlemsucaccv  6426  tfrcllemsucaccv  6439  oav2  6548  omv2  6550  fnsnsplitdc  6590  ecopovtrn  6718  ecopovtrng  6721  map0b  6773  en1  6890  ssenen  6947  fidifsnen  6966  dif1en  6975  undifdc  7020  fidcenumlemr  7056  ordiso2  7136  nninfninc  7224  nnnninfeq2  7230  nninfisollemne  7232  finomni  7241  exmidomni  7243  fodjum  7247  exmidaclem  7319  distrnqg  7499  1qec  7500  prarloclemarch2  7531  nnnq0lem1  7558  nqpnq0nq  7565  distrnq0  7571  prarloclemlt  7605  prmuloclemcalc  7677  ltaprg  7731  prplnqu  7732  recexprlem1ssl  7745  recexprlem1ssu  7746  ltmprr  7754  cauappcvgprlemopl  7758  caucvgprlemopl  7781  caucvgprprlemopl  7809  caucvgprprlemexb  7819  prsrlem1  7854  ltsosr  7876  mulgt0sr  7890  recidpipr  7968  recriota  8002  nntopi  8006  axcaucvglemres  8011  addlid  8210  readdcan  8211  muladd11r  8227  add32r  8231  cnegexlem2  8247  cnegex  8249  pncan2  8278  addsubass  8281  subadd23  8283  addsub12  8284  subid  8290  subid1  8291  npncan  8292  nppcan3  8295  subsub  8301  nppcan2  8302  nnncan2  8308  npncan3  8309  pnpcan  8310  negdi  8328  mvlraddd  8435  mvlladdd  8436  pnpncand  8446  subdi  8456  mulsub  8472  mulsub2  8473  eqord1  8555  recexap  8725  div32ap  8764  divsubdirap  8780  divmuldivap  8784  divdivdivap  8785  divmuleqap  8789  divcanap6  8791  dmdcanap  8794  divsubdivap  8800  div2negap  8807  div2subap  8909  mvllmulapd  8914  prodgt0gt0  8923  cju  9033  zneo  9473  infrenegsupex  9714  qreccl  9762  mul2lt0rlt0  9880  xnpcan  9993  fzosn  10332  modqid  10492  modqm1p1mod0  10518  modqltm1p1mod  10519  modqmul1  10520  modaddmodup  10530  modaddmodlo  10531  modqsubdir  10536  iseqf1olemkle  10640  iseqf1olemklt  10641  seq3f1olemstep  10657  seq3f1oleml  10659  seqf1oglem2  10663  seqfeq3  10672  seq3distr  10675  expineg2  10691  expm1t  10710  expadd  10724  expaddzaplem  10725  expmulzap  10728  sqsubswap  10742  subsq2  10790  binom2sub  10796  binom3  10800  facndiv  10882  bcval5  10906  bcn2p1  10913  bcnm1  10915  2shfti  11113  shftcan2  11117  reim0  11143  imval2  11176  cjreim2  11186  cjdivap  11191  cnrecnv  11192  rennim  11284  resqrexlemnm  11300  remsqsqrt  11314  sqrtdiv  11324  sqrtmsq  11327  sqabsadd  11337  sqabssub  11338  absreim  11350  absdivap  11352  absnid  11355  sqabs  11364  abslt  11370  absle  11371  recvalap  11379  abssub  11383  maxabslemlub  11489  infxrnegsupex  11545  mulcn2  11594  reccn2ap  11595  cjcn2  11598  summodclem3  11662  summodclem2a  11663  summodc  11665  zsumdc  11666  fsum3  11669  fisumss  11674  fsumcl2lem  11680  fsumm1  11698  fsum1p  11700  isummulc2  11708  telfsumo  11748  binomlem  11765  bcxmas  11771  arisum  11780  trireciplem  11782  trirecip  11783  geolim2  11794  georeclim  11795  cvgratnnlemfm  11811  cvgratz  11814  mertenslemi1  11817  clim2divap  11822  prodmodclem3  11857  prodmodclem2a  11858  zproddc  11861  fprodseq  11865  fprodssdc  11872  fprod1p  11881  efcan  11958  efexp  11964  efzval  11965  efgt0  11966  eftlub  11972  efltim  11980  resinval  11997  recosval  11998  cosmul  12027  cos2t  12032  cos2tsin  12033  cos01bnd  12040  cos12dec  12050  eirraplem  12059  muldvds1  12098  dvdsexp  12143  oexpneg  12159  divalglemqt  12201  divalglemeunn  12203  divalglemeuneg  12205  divalgmod  12209  flodddiv4t2lthalf  12221  bitsmod  12238  bitsinv1lem  12243  gcdid0  12272  gcdaddm  12276  dvdsgcdidd  12286  rpmulgcd  12318  sqgcd  12321  algcvg  12341  eucalgcvga  12351  eucalg  12352  dvdslcm  12362  lcmeq0  12364  lcmgcd  12371  qredeu  12390  sqnprm  12429  divgcdodd  12436  sqrt2irrlem  12454  sqpweven  12468  2sqpwodd  12469  divnumden  12489  hashdvds  12514  phimullem  12518  eulerthlemrprm  12522  eulerthlemth  12525  odzdvds  12539  pythagtriplem3  12561  pythagtriplem4  12562  pythagtriplem14  12571  pythagtriplem19  12576  pcpremul  12587  pceulem  12588  pcqdiv  12601  pcaddlem  12633  fldivp1  12642  1arithlem4  12660  4sqlem10  12681  mul4sqlem  12687  4sqlem11  12695  4sqlem15  12699  4sqlem16  12700  4sqlem17  12701  ennnfonelemhf1o  12755  strslssd  12850  ressbas2d  12871  ressinbasd  12877  topnidg  13055  lidrideqd  13184  grpidd  13186  grprida  13190  gsumress  13198  ismndd  13240  grpidd2  13344  grpinvid1  13355  grpinvid2  13356  grppnpcan2  13397  grpnpncan  13398  dfgrp3mlem  13401  grpsubpropd2  13408  mhmid  13422  mhmmnd  13423  mulgsubcl  13443  mulgneg  13447  mulgaddcomlem  13452  mulginvinv  13455  mulgdirlem  13460  mulgdir  13461  mulgass  13466  mulgmodid  13468  grpissubg  13501  eqgcpbl  13535  ghmid  13556  ghmmulg  13563  resghm  13567  invghm  13636  gsumfzmptfidmadd  13646  mgptopng  13662  srgisid  13719  ringidss  13762  ringcom  13764  opprsubgg  13817  unitgrp  13849  1rinv  13861  0unit  13862  rhmdvdsr  13908  lringuplu  13929  subrngpropd  13949  subrgpropd  13986  lmod0vs  14054  lmodvsmmulgdi  14056  lmodvneg1  14063  lmodcom  14066  lmodsubvs  14076  lmodsubdir  14078  lmodpropd  14082  lspsnsub  14154  lspsneq0b  14160  lsppropd  14165  rlmscabas  14193  lidlbas  14211  zringmulg  14331  restopnb  14624  txcnmpt  14716  cnmpt1t  14728  blhalf  14851  xmspropd  14920  mspropd  14921  mpomulcn  15009  ivthreinc  15088  limcimolemlt  15107  dvfre  15153  dveflem  15169  dvef  15170  ply1termlem  15185  plymullem1  15191  sin2kpi  15254  cos2kpi  15255  sin2pim  15256  cos2pim  15257  ptolemy  15267  sincosq2sgn  15270  sincosq3sgn  15271  sincosq4sgn  15272  sinq12gt0  15273  tangtx  15281  sincosq1eq  15282  abssinper  15289  sinkpi  15290  relogeftb  15308  relogoprlem  15311  relogexp  15315  mpodvdsmulf1o  15433  mersenne  15440  perfectlem1  15442  perfectlem2  15443  perfect  15444  lgsval2lem  15458  lgsdir2lem4  15479  lgsdirprm  15482  lgsdilem2  15484  gausslemma2dlem7  15516  lgseisenlem4  15521  lgsquadlem1  15525  lgsquadlem2  15526  lgsquad2lem1  15529  lgsquad2lem2  15530  2sqlem4  15566  2sqlem6  15568  2sqlem8  15571  peano3nninf  15906  nninfsel  15916  nninffeq  15919  isomninnlem  15931  cvgcmp2nlemabs  15933  trilpolemlt1  15942  trirec0xor  15946  ismkvnnlem  15953