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  6600  tfr1onlemsucaccv  6616  tfrcllemsucaccv  6629  oav2  6740  omv2  6742  fnsnsplitdc  6782  ecopovtrn  6910  ecopovtrng  6913  map0b  6972  en1  7090  ssenen  7156  fidifsnen  7176  dif1en  7187  undifdc  7235  fidcenumlemr  7277  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  9758  infrenegsupex  10010  qreccl  10058  mul2lt0rlt0  10177  xnpcan  10291  fzosn  10640  modqid  10807  modqm1p1mod0  10833  modqltm1p1mod  10834  modqmul1  10835  modaddmodup  10845  modaddmodlo  10846  modqsubdir  10851  iseqf1olemkle  10955  iseqf1olemklt  10956  seq3f1olemstep  10972  seq3f1oleml  10974  seqf1oglem2  10978  seqfeq3  10987  seq3distr  10990  expineg2  11006  expm1t  11025  expadd  11039  expaddzaplem  11040  expmulzap  11043  sqsubswap  11057  subsq2  11105  binom2sub  11111  binom3  11115  resq01  11116  facndiv  11199  bcval5  11223  bcn2p1  11231  bcnm1  11233  hashpwfi  11291  hashfibclem  11304  pfxccatpfx2  11531  2shfti  11618  shftcan2  11622  reim0  11648  imval2  11681  cjreim2  11692  cjdivap  11697  cnrecnv  11698  rennim  11790  resqrexlemnm  11806  remsqsqrt  11820  sqrtdiv  11830  sqrtmsq  11833  sqabsadd  11843  sqabssub  11844  absreim  11856  absdivap  11858  absnid  11861  sqabs  11871  abslt  11877  absle  11878  recvalap  11886  abssub  11890  maxabslemlub  11996  infxrnegsupex  12054  mulcn2  12103  reccn2ap  12104  cjcn2  12107  summodclem3  12172  summodclem2a  12173  summodc  12175  zsumdc  12176  fsum3  12179  fisumss  12184  fsumcl2lem  12190  fsumm1  12208  fsum1p  12210  isummulc2  12218  telfsumo  12258  binomlem  12275  bcxmas  12281  arisum  12290  trireciplem  12292  trirecip  12293  geolim2  12304  georeclim  12305  cvgratnnlemfm  12321  cvgratz  12324  mertenslemi1  12327  clim2divap  12332  prodmodclem3  12367  prodmodclem2a  12368  zproddc  12371  fprodseq  12375  fprodssdc  12382  fprod1p  12391  efcan  12468  efexp  12474  efzval  12475  efgt0  12476  eftlub  12482  efltim  12490  resinval  12507  recosval  12508  cosmul  12537  cos2t  12542  cos2tsin  12543  cos01bnd  12550  cos12dec  12560  eirraplem  12569  muldvds1  12608  dvdsexp  12653  oexpneg  12669  divalglemqt  12711  divalglemeunn  12713  divalglemeuneg  12715  divalgmod  12719  flodddiv4t2lthalf  12731  bitsmod  12748  bitsinv1lem  12753  gcdid0  12782  gcdaddm  12786  dvdsgcdidd  12796  rpmulgcd  12828  sqgcd  12831  algcvg  12851  eucalgcvga  12861  eucalg  12862  dvdslcm  12872  lcmeq0  12874  lcmgcd  12881  qredeu  12900  sqnprm  12940  divgcdodd  12947  sqrt2irrlem  12965  sqpweven  12980  2sqpwodd  12981  divnumden  13001  hashdvds  13028  phimullem  13032  eulerthlemrprm  13036  eulerthlemth  13039  odzdvds  13053  pythagtriplem3  13075  pythagtriplem4  13076  pythagtriplem14  13085  pythagtriplem19  13090  pcpremul  13101  pceulem  13102  pcqdiv  13115  pcaddlem  13147  fldivp1  13156  1arithlem4  13174  4sqlem10  13195  mul4sqlem  13201  4sqlem11  13209  4sqlem15  13213  4sqlem16  13214  4sqlem17  13215  ballotfilemfc0  13290  ballotfilemfcc  13291  ballotfilemic  13308  ballotfilem1c  13309  ballotfilemfrceq  13330  ballotfilemrinv0  13334  ennnfonelemhf1o  13362  strslssd  13457  ressbas2d  13481  ressinbasd  13487  topnidg  13665  lidrideqd  13760  grpidd  13762  grprida  13766  gzsumress  13771  ismndd  13809  grpidd2  13905  grpinvid1  13916  grpinvid2  13917  grppnpcan2  13958  grpnpncan  13959  dfgrp3mlem  13962  grpsubpropd2  13969  mhmid  13977  mhmmnd  13978  mulgsubcl  13998  mulgneg  14002  mulgaddcomlem  14007  mulginvinv  14010  mulgdirlem  14015  mulgdir  14016  mulgass  14021  mulgmodid  14023  grpissubg  14056  eqgcpbl  14090  ghmid  14111  ghmmulg  14118  resghm  14122  cntrsubgnsg  14175  invghm  14223  gsum0cmn  14244  gsumresfi  14263  gsum2dfilem2  14272  mgptopng  14335  srgisid  14397  ringidss  14441  ringcom  14443  opprsubgg  14499  unitgrp  14532  1rinv  14544  0unit  14545  rhmdvdsr  14591  lringuplu  14612  subrngpropd  14633  subrgpropd  14670  lmod0vs  14767  lmodvsmmulgdi  14769  lmodvneg1  14776  lmodcom  14779  lmodsubvs  14789  lmodsubdir  14791  lmodpropd  14795  lspsnsub  14867  lspsneq0b  14873  lsppropd  14878  rlmscabas  14906  lidlbas  14924  zringmulg  15042  restopnb  15407  txcnmpt  15499  cnmpt1t  15511  blhalf  15634  xmspropd  15703  mspropd  15704  mpomulcn  15792  ivthreinc  15871  limcimolemlt  15890  dvfre  15936  dveflem  15952  dvef  15953  ply1termlem  15968  plymullem1  15974  sin2kpi  16038  cos2kpi  16039  sin2pim  16040  cos2pim  16041  ptolemy  16051  sincosq2sgn  16054  sincosq3sgn  16055  sincosq4sgn  16056  sinq12gt0  16057  tangtx  16065  sincosq1eq  16066  abssinper  16073  sinkpi  16074  sineq0re  16076  root1idef  16084  relogeftb  16094  relogoprlem  16098  relogexp  16102  rpcxpmul2z  16148  log2tlbndlog2  16220  birthdaylem2  16226  birthdaylem3  16227  pellexlem1  16229  efchtqdvds  16265  ppiqp1le  16267  ppiqltx  16281  mpodvdsmulf1o  16284  ppiqub  16293  chtqub  16296  mersenne  16297  perfectlem1  16299  perfectlem2  16300  perfect  16301  bposlem6  16316  bposlem9  16319  lgsval2lem  16334  lgsdir2lem4  16355  lgsdirprm  16358  lgsdilem2  16360  gausslemma2dlem7  16392  lgseisenlem4  16397  lgsquadlem1  16401  lgsquadlem2  16402  lgsquad2lem1  16405  lgsquad2lem2  16406  2sqlem4  16442  2sqlem6  16444  2sqlem8  16447  clwwlknonel  16878  eupth2fi  16925  dichmul0orlem2  16959  dichmul0orlem3  16960  dichmul0orlem4  16961  peano3nninf  17256  nninfsel  17266  nninffeq  17269  isomninnlem  17285  cvgcmp2nlemabs  17287  trilpolemlt1  17297  trirec0xor  17301  qdiff  17305  ismkvnnlem  17309