Theorem eqtr3d 2205

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

Syntax hints:   -> wi 4   = wceq 1348

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-gen 1442  ax-4 1503  ax-17 1519  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-cleq 2163

This theorem is referenced by:  3eqtr3d  2211  3eqtr3rd  2212  3eqtr3a  2227  opth  4222  eusvnf  4438  f00  5389  f1imacnv  5459  foimacnv  5460  f1ococnv1  5471  funfvdm  5559  fvmptdf  5583  fndmdif  5601  acexmidlemph  5846  acexmidlemab  5847  ovmpodf  5984  oprssov  5994  tfrlemisucaccv  6304  tfr1onlemsucaccv  6320  tfrcllemsucaccv  6333  oav2  6442  omv2  6444  fnsnsplitdc  6484  ecopovtrn  6610  ecopovtrng  6613  map0b  6665  en1  6777  ssenen  6829  fidifsnen  6848  dif1en  6857  undifdc  6901  fidcenumlemr  6932  ordiso2  7012  nnnninfeq2  7105  nninfisollemne  7107  finomni  7116  exmidomni  7118  fodjum  7122  exmidaclem  7185  distrnqg  7349  1qec  7350  prarloclemarch2  7381  nnnq0lem1  7408  nqpnq0nq  7415  distrnq0  7421  prarloclemlt  7455  prmuloclemcalc  7527  ltaprg  7581  prplnqu  7582  recexprlem1ssl  7595  recexprlem1ssu  7596  ltmprr  7604  cauappcvgprlemopl  7608  caucvgprlemopl  7631  caucvgprprlemopl  7659  caucvgprprlemexb  7669  prsrlem1  7704  ltsosr  7726  mulgt0sr  7740  recidpipr  7818  recriota  7852  nntopi  7856  axcaucvglemres  7861  addid2  8058  readdcan  8059  muladd11r  8075  add32r  8079  cnegexlem2  8095  cnegex  8097  pncan2  8126  addsubass  8129  subadd23  8131  addsub12  8132  subid  8138  subid1  8139  npncan  8140  nppcan3  8143  subsub  8149  nppcan2  8150  nnncan2  8156  npncan3  8157  pnpcan  8158  negdi  8176  mvlraddd  8283  mvlladdd  8284  pnpncand  8294  subdi  8304  mulsub  8320  mulsub2  8321  eqord1  8402  recexap  8571  div32ap  8609  divsubdirap  8625  divmuldivap  8629  divdivdivap  8630  divmuleqap  8634  divcanap6  8636  dmdcanap  8639  divsubdivap  8645  div2negap  8652  div2subap  8754  mvllmulapd  8759  prodgt0gt0  8767  cju  8877  zneo  9313  infrenegsupex  9553  qreccl  9601  mul2lt0rlt0  9716  xnpcan  9829  fzosn  10161  modqid  10305  modqm1p1mod0  10331  modqltm1p1mod  10332  modqmul1  10333  modaddmodup  10343  modaddmodlo  10344  modqsubdir  10349  iseqf1olemkle  10440  iseqf1olemklt  10441  seq3f1olemstep  10457  seq3f1oleml  10459  seqfeq3  10468  seq3distr  10469  expineg2  10485  expm1t  10504  expadd  10518  expaddzaplem  10519  expmulzap  10522  sqsubswap  10536  subsq2  10583  binom2sub  10589  binom3  10593  facndiv  10673  bcval5  10697  bcn2p1  10704  bcnm1  10706  2shfti  10795  shftcan2  10799  reim0  10825  imval2  10858  cjreim2  10868  cjdivap  10873  cnrecnv  10874  rennim  10966  resqrexlemnm  10982  remsqsqrt  10996  sqrtdiv  11006  sqrtmsq  11009  sqabsadd  11019  sqabssub  11020  absreim  11032  absdivap  11034  absnid  11037  sqabs  11046  abslt  11052  absle  11053  recvalap  11061  abssub  11065  maxabslemlub  11171  infxrnegsupex  11226  mulcn2  11275  reccn2ap  11276  cjcn2  11279  summodclem3  11343  summodclem2a  11344  summodc  11346  zsumdc  11347  fsum3  11350  fisumss  11355  fsumcl2lem  11361  fsumm1  11379  fsum1p  11381  isummulc2  11389  telfsumo  11429  binomlem  11446  bcxmas  11452  arisum  11461  trireciplem  11463  trirecip  11464  geolim2  11475  georeclim  11476  cvgratnnlemfm  11492  cvgratz  11495  mertenslemi1  11498  clim2divap  11503  prodmodclem3  11538  prodmodclem2a  11539  zproddc  11542  fprodseq  11546  fprodssdc  11553  fprod1p  11562  efcan  11639  efexp  11645  efzval  11646  efgt0  11647  eftlub  11653  efltim  11661  resinval  11678  recosval  11679  cosmul  11708  cos2t  11713  cos2tsin  11714  cos01bnd  11721  cos12dec  11730  eirraplem  11739  muldvds1  11778  dvdsexp  11821  oexpneg  11836  divalglemqt  11878  divalglemeunn  11880  divalglemeuneg  11882  divalgmod  11886  flodddiv4t2lthalf  11896  gcdid0  11935  gcdaddm  11939  dvdsgcdidd  11949  rpmulgcd  11981  sqgcd  11984  algcvg  12002  eucalgcvga  12012  eucalg  12013  dvdslcm  12023  lcmeq0  12025  lcmgcd  12032  qredeu  12051  sqnprm  12090  divgcdodd  12097  sqrt2irrlem  12115  sqpweven  12129  2sqpwodd  12130  divnumden  12150  hashdvds  12175  phimullem  12179  eulerthlemrprm  12183  eulerthlemth  12186  odzdvds  12199  pythagtriplem3  12221  pythagtriplem4  12222  pythagtriplem14  12231  pythagtriplem19  12236  pcpremul  12247  pceulem  12248  pcqdiv  12261  pcaddlem  12292  fldivp1  12300  1arithlem4  12318  4sqlem10  12339  mul4sqlem  12345  ennnfonelemhf1o  12368  strslssd  12462  topnidg  12592  lidrideqd  12635  grpidd  12637  grpridd  12641  ismndd  12673  grpidd2  12744  grpinvid1  12754  grpinvid2  12755  restopnb  12975  txcnmpt  13067  cnmpt1t  13079  blhalf  13202  xmspropd  13271  mspropd  13272  limcimolemlt  13427  dvfre  13468  dveflem  13481  dvef  13482  sin2kpi  13526  cos2kpi  13527  sin2pim  13528  cos2pim  13529  ptolemy  13539  sincosq2sgn  13542  sincosq3sgn  13543  sincosq4sgn  13544  sinq12gt0  13545  tangtx  13553  sincosq1eq  13554  abssinper  13561  sinkpi  13562  relogeftb  13580  relogoprlem  13583  relogexp  13587  lgsval2lem  13705  lgsdir2lem4  13726  lgsdirprm  13729  lgsdilem2  13731  2sqlem4  13748  2sqlem6  13750  2sqlem8  13753  peano3nninf  14040  nninfsel  14050  nninffeq  14053  isomninnlem  14062  cvgcmp2nlemabs  14064  trilpolemlt1  14073  trirec0xor  14077  ismkvnnlem  14084