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  4220  eusvnf  4436  f00  5387  f1imacnv  5457  foimacnv  5458  f1ococnv1  5469  funfvdm  5557  fvmptdf  5581  fndmdif  5598  acexmidlemph  5843  acexmidlemab  5844  ovmpodf  5981  oprssov  5991  tfrlemisucaccv  6301  tfr1onlemsucaccv  6317  tfrcllemsucaccv  6330  oav2  6439  omv2  6441  fnsnsplitdc  6481  ecopovtrn  6606  ecopovtrng  6609  map0b  6661  en1  6773  ssenen  6825  fidifsnen  6844  dif1en  6853  undifdc  6897  fidcenumlemr  6928  ordiso2  7008  nnnninfeq2  7101  nninfisollemne  7103  finomni  7112  exmidomni  7114  fodjum  7118  exmidaclem  7172  distrnqg  7336  1qec  7337  prarloclemarch2  7368  nnnq0lem1  7395  nqpnq0nq  7402  distrnq0  7408  prarloclemlt  7442  prmuloclemcalc  7514  ltaprg  7568  prplnqu  7569  recexprlem1ssl  7582  recexprlem1ssu  7583  ltmprr  7591  cauappcvgprlemopl  7595  caucvgprlemopl  7618  caucvgprprlemopl  7646  caucvgprprlemexb  7656  prsrlem1  7691  ltsosr  7713  mulgt0sr  7727  recidpipr  7805  recriota  7839  nntopi  7843  axcaucvglemres  7848  addid2  8045  readdcan  8046  muladd11r  8062  add32r  8066  cnegexlem2  8082  cnegex  8084  pncan2  8113  addsubass  8116  subadd23  8118  addsub12  8119  subid  8125  subid1  8126  npncan  8127  nppcan3  8130  subsub  8136  nppcan2  8137  nnncan2  8143  npncan3  8144  pnpcan  8145  negdi  8163  mvlraddd  8270  mvlladdd  8271  pnpncand  8281  subdi  8291  mulsub  8307  mulsub2  8308  eqord1  8389  recexap  8558  div32ap  8596  divsubdirap  8612  divmuldivap  8616  divdivdivap  8617  divmuleqap  8621  divcanap6  8623  dmdcanap  8626  divsubdivap  8632  div2negap  8639  div2subap  8741  mvllmulapd  8746  prodgt0gt0  8754  cju  8864  zneo  9300  infrenegsupex  9540  qreccl  9588  mul2lt0rlt0  9703  xnpcan  9816  fzosn  10148  modqid  10292  modqm1p1mod0  10318  modqltm1p1mod  10319  modqmul1  10320  modaddmodup  10330  modaddmodlo  10331  modqsubdir  10336  iseqf1olemkle  10427  iseqf1olemklt  10428  seq3f1olemstep  10444  seq3f1oleml  10446  seqfeq3  10455  seq3distr  10456  expineg2  10472  expm1t  10491  expadd  10505  expaddzaplem  10506  expmulzap  10509  sqsubswap  10523  subsq2  10570  binom2sub  10576  binom3  10580  facndiv  10660  bcval5  10684  bcn2p1  10691  bcnm1  10693  2shfti  10782  shftcan2  10786  reim0  10812  imval2  10845  cjreim2  10855  cjdivap  10860  cnrecnv  10861  rennim  10953  resqrexlemnm  10969  remsqsqrt  10983  sqrtdiv  10993  sqrtmsq  10996  sqabsadd  11006  sqabssub  11007  absreim  11019  absdivap  11021  absnid  11024  sqabs  11033  abslt  11039  absle  11040  recvalap  11048  abssub  11052  maxabslemlub  11158  infxrnegsupex  11213  mulcn2  11262  reccn2ap  11263  cjcn2  11266  summodclem3  11330  summodclem2a  11331  summodc  11333  zsumdc  11334  fsum3  11337  fisumss  11342  fsumcl2lem  11348  fsumm1  11366  fsum1p  11368  isummulc2  11376  telfsumo  11416  binomlem  11433  bcxmas  11439  arisum  11448  trireciplem  11450  trirecip  11451  geolim2  11462  georeclim  11463  cvgratnnlemfm  11479  cvgratz  11482  mertenslemi1  11485  clim2divap  11490  prodmodclem3  11525  prodmodclem2a  11526  zproddc  11529  fprodseq  11533  fprodssdc  11540  fprod1p  11549  efcan  11626  efexp  11632  efzval  11633  efgt0  11634  eftlub  11640  efltim  11648  resinval  11665  recosval  11666  cosmul  11695  cos2t  11700  cos2tsin  11701  cos01bnd  11708  cos12dec  11717  eirraplem  11726  muldvds1  11765  dvdsexp  11808  oexpneg  11823  divalglemqt  11865  divalglemeunn  11867  divalglemeuneg  11869  divalgmod  11873  flodddiv4t2lthalf  11883  gcdid0  11922  gcdaddm  11926  dvdsgcdidd  11936  rpmulgcd  11968  sqgcd  11971  algcvg  11989  eucalgcvga  11999  eucalg  12000  dvdslcm  12010  lcmeq0  12012  lcmgcd  12019  qredeu  12038  sqnprm  12077  divgcdodd  12084  sqrt2irrlem  12102  sqpweven  12116  2sqpwodd  12117  divnumden  12137  hashdvds  12162  phimullem  12166  eulerthlemrprm  12170  eulerthlemth  12173  odzdvds  12186  pythagtriplem3  12208  pythagtriplem4  12209  pythagtriplem14  12218  pythagtriplem19  12223  pcpremul  12234  pceulem  12235  pcqdiv  12248  pcaddlem  12279  fldivp1  12287  1arithlem4  12305  4sqlem10  12326  mul4sqlem  12332  ennnfonelemhf1o  12355  strslssd  12449  topnidg  12579  lidrideqd  12622  grpidd  12624  grpridd  12628  ismndd  12660  grpidd2  12731  restopnb  12934  txcnmpt  13026  cnmpt1t  13038  blhalf  13161  xmspropd  13230  mspropd  13231  limcimolemlt  13386  dvfre  13427  dveflem  13440  dvef  13441  sin2kpi  13485  cos2kpi  13486  sin2pim  13487  cos2pim  13488  ptolemy  13498  sincosq2sgn  13501  sincosq3sgn  13502  sincosq4sgn  13503  sinq12gt0  13504  tangtx  13512  sincosq1eq  13513  abssinper  13520  sinkpi  13521  relogeftb  13539  relogoprlem  13542  relogexp  13546  lgsval2lem  13664  lgsdir2lem4  13685  lgsdirprm  13688  lgsdilem2  13690  2sqlem4  13707  2sqlem6  13709  2sqlem8  13712  peano3nninf  14000  nninfsel  14010  nninffeq  14013  isomninnlem  14022  cvgcmp2nlemabs  14024  trilpolemlt1  14033  trirec0xor  14037  ismkvnnlem  14044