Theorem eqtr3d 2212

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

Syntax hints:   -> wi 4   = wceq 1353

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 1447  ax-gen 1449  ax-4 1510  ax-17 1526  ax-ext 2159

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

This theorem is referenced by:  3eqtr3d  2218  3eqtr3rd  2219  3eqtr3a  2234  opth  4239  eusvnf  4455  f00  5409  f1imacnv  5480  foimacnv  5481  f1ococnv1  5492  funfvdm  5581  fvmptdf  5605  fndmdif  5623  acexmidlemph  5870  acexmidlemab  5871  ovmpodf  6008  oprssov  6018  tfrlemisucaccv  6328  tfr1onlemsucaccv  6344  tfrcllemsucaccv  6357  oav2  6466  omv2  6468  fnsnsplitdc  6508  ecopovtrn  6634  ecopovtrng  6637  map0b  6689  en1  6801  ssenen  6853  fidifsnen  6872  dif1en  6881  undifdc  6925  fidcenumlemr  6956  ordiso2  7036  nnnninfeq2  7129  nninfisollemne  7131  finomni  7140  exmidomni  7142  fodjum  7146  exmidaclem  7209  distrnqg  7388  1qec  7389  prarloclemarch2  7420  nnnq0lem1  7447  nqpnq0nq  7454  distrnq0  7460  prarloclemlt  7494  prmuloclemcalc  7566  ltaprg  7620  prplnqu  7621  recexprlem1ssl  7634  recexprlem1ssu  7635  ltmprr  7643  cauappcvgprlemopl  7647  caucvgprlemopl  7670  caucvgprprlemopl  7698  caucvgprprlemexb  7708  prsrlem1  7743  ltsosr  7765  mulgt0sr  7779  recidpipr  7857  recriota  7891  nntopi  7895  axcaucvglemres  7900  addlid  8098  readdcan  8099  muladd11r  8115  add32r  8119  cnegexlem2  8135  cnegex  8137  pncan2  8166  addsubass  8169  subadd23  8171  addsub12  8172  subid  8178  subid1  8179  npncan  8180  nppcan3  8183  subsub  8189  nppcan2  8190  nnncan2  8196  npncan3  8197  pnpcan  8198  negdi  8216  mvlraddd  8323  mvlladdd  8324  pnpncand  8334  subdi  8344  mulsub  8360  mulsub2  8361  eqord1  8442  recexap  8612  div32ap  8651  divsubdirap  8667  divmuldivap  8671  divdivdivap  8672  divmuleqap  8676  divcanap6  8678  dmdcanap  8681  divsubdivap  8687  div2negap  8694  div2subap  8796  mvllmulapd  8801  prodgt0gt0  8810  cju  8920  zneo  9356  infrenegsupex  9596  qreccl  9644  mul2lt0rlt0  9761  xnpcan  9874  fzosn  10207  modqid  10351  modqm1p1mod0  10377  modqltm1p1mod  10378  modqmul1  10379  modaddmodup  10389  modaddmodlo  10390  modqsubdir  10395  iseqf1olemkle  10486  iseqf1olemklt  10487  seq3f1olemstep  10503  seq3f1oleml  10505  seqfeq3  10514  seq3distr  10515  expineg2  10531  expm1t  10550  expadd  10564  expaddzaplem  10565  expmulzap  10568  sqsubswap  10582  subsq2  10630  binom2sub  10636  binom3  10640  facndiv  10721  bcval5  10745  bcn2p1  10752  bcnm1  10754  2shfti  10842  shftcan2  10846  reim0  10872  imval2  10905  cjreim2  10915  cjdivap  10920  cnrecnv  10921  rennim  11013  resqrexlemnm  11029  remsqsqrt  11043  sqrtdiv  11053  sqrtmsq  11056  sqabsadd  11066  sqabssub  11067  absreim  11079  absdivap  11081  absnid  11084  sqabs  11093  abslt  11099  absle  11100  recvalap  11108  abssub  11112  maxabslemlub  11218  infxrnegsupex  11273  mulcn2  11322  reccn2ap  11323  cjcn2  11326  summodclem3  11390  summodclem2a  11391  summodc  11393  zsumdc  11394  fsum3  11397  fisumss  11402  fsumcl2lem  11408  fsumm1  11426  fsum1p  11428  isummulc2  11436  telfsumo  11476  binomlem  11493  bcxmas  11499  arisum  11508  trireciplem  11510  trirecip  11511  geolim2  11522  georeclim  11523  cvgratnnlemfm  11539  cvgratz  11542  mertenslemi1  11545  clim2divap  11550  prodmodclem3  11585  prodmodclem2a  11586  zproddc  11589  fprodseq  11593  fprodssdc  11600  fprod1p  11609  efcan  11686  efexp  11692  efzval  11693  efgt0  11694  eftlub  11700  efltim  11708  resinval  11725  recosval  11726  cosmul  11755  cos2t  11760  cos2tsin  11761  cos01bnd  11768  cos12dec  11777  eirraplem  11786  muldvds1  11825  dvdsexp  11869  oexpneg  11884  divalglemqt  11926  divalglemeunn  11928  divalglemeuneg  11930  divalgmod  11934  flodddiv4t2lthalf  11944  gcdid0  11983  gcdaddm  11987  dvdsgcdidd  11997  rpmulgcd  12029  sqgcd  12032  algcvg  12050  eucalgcvga  12060  eucalg  12061  dvdslcm  12071  lcmeq0  12073  lcmgcd  12080  qredeu  12099  sqnprm  12138  divgcdodd  12145  sqrt2irrlem  12163  sqpweven  12177  2sqpwodd  12178  divnumden  12198  hashdvds  12223  phimullem  12227  eulerthlemrprm  12231  eulerthlemth  12234  odzdvds  12247  pythagtriplem3  12269  pythagtriplem4  12270  pythagtriplem14  12279  pythagtriplem19  12284  pcpremul  12295  pceulem  12296  pcqdiv  12309  pcaddlem  12340  fldivp1  12348  1arithlem4  12366  4sqlem10  12387  mul4sqlem  12393  ennnfonelemhf1o  12416  strslssd  12511  ressbas2d  12530  ressinbasd  12535  topnidg  12706  lidrideqd  12805  grpidd  12807  grpridd  12811  ismndd  12843  grpidd2  12919  grpinvid1  12929  grpinvid2  12930  grppnpcan2  12969  grpnpncan  12970  dfgrp3mlem  12973  grpsubpropd2  12980  mhmid  12984  mhmmnd  12985  mulgsubcl  13002  mulgneg  13006  mulgaddcomlem  13011  mulginvinv  13014  mulgdirlem  13019  mulgdir  13020  mulgass  13025  mulgmodid  13027  grpissubg  13059  eqgcpbl  13092  mgptopng  13144  srgisid  13174  ringidss  13217  ringcom  13219  unitgrp  13290  1rinv  13302  0unit  13303  lringuplu  13342  subrgpropd  13374  lmod0vs  13416  lmodvsmmulgdi  13418  lmodvneg1  13425  lmodcom  13428  lmodsubvs  13438  lmodsubdir  13440  lmodpropd  13444  zringmulg  13527  restopnb  13720  txcnmpt  13812  cnmpt1t  13824  blhalf  13947  xmspropd  14016  mspropd  14017  limcimolemlt  14172  dvfre  14213  dveflem  14226  dvef  14227  sin2kpi  14271  cos2kpi  14272  sin2pim  14273  cos2pim  14274  ptolemy  14284  sincosq2sgn  14287  sincosq3sgn  14288  sincosq4sgn  14289  sinq12gt0  14290  tangtx  14298  sincosq1eq  14299  abssinper  14306  sinkpi  14307  relogeftb  14325  relogoprlem  14328  relogexp  14332  lgsval2lem  14450  lgsdir2lem4  14471  lgsdirprm  14474  lgsdilem2  14476  2sqlem4  14504  2sqlem6  14506  2sqlem8  14509  peano3nninf  14795  nninfsel  14805  nninffeq  14808  isomninnlem  14817  cvgcmp2nlemabs  14819  trilpolemlt1  14828  trirec0xor  14832  ismkvnnlem  14839