Theorem eqtr3d 2134

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

Syntax hints:   -> wi 4   = wceq 1299

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1391  ax-gen 1393  ax-4 1455  ax-17 1474  ax-ext 2082

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

This theorem is referenced by:  3eqtr3d  2140  3eqtr3rd  2141  3eqtr3a  2156  opth  4097  eusvnf  4312  f00  5250  f1imacnv  5318  foimacnv  5319  f1ococnv1  5330  funfvdm  5416  fvmptdf  5440  fndmdif  5457  acexmidlemph  5699  acexmidlemab  5700  ovmpodf  5834  oprssov  5844  grpridd  5899  tfrlemisucaccv  6152  tfr1onlemsucaccv  6168  tfrcllemsucaccv  6181  oav2  6289  omv2  6291  fnsnsplitdc  6331  ecopovtrn  6456  ecopovtrng  6459  map0b  6511  en1  6623  ssenen  6674  fidifsnen  6693  dif1en  6702  undifdc  6741  fidcenumlemr  6771  ordiso2  6835  finomni  6924  exmidomni  6926  fodjum  6930  distrnqg  7096  1qec  7097  prarloclemarch2  7128  nnnq0lem1  7155  nqpnq0nq  7162  distrnq0  7168  prarloclemlt  7202  prmuloclemcalc  7274  ltaprg  7328  prplnqu  7329  recexprlem1ssl  7342  recexprlem1ssu  7343  ltmprr  7351  cauappcvgprlemopl  7355  caucvgprlemopl  7378  caucvgprprlemopl  7406  caucvgprprlemexb  7416  prsrlem1  7438  ltsosr  7460  mulgt0sr  7473  recidpipr  7543  recriota  7575  nntopi  7579  axcaucvglemres  7584  addid2  7772  readdcan  7773  muladd11r  7789  add32r  7793  cnegexlem2  7809  cnegex  7811  pncan2  7840  addsubass  7843  subadd23  7845  addsub12  7846  subid  7852  subid1  7853  npncan  7854  nppcan3  7857  subsub  7863  nppcan2  7864  nnncan2  7870  npncan3  7871  pnpcan  7872  negdi  7890  mvlraddd  7996  pnpncand  8004  subdi  8014  mulsub  8030  mulsub2  8031  eqord1  8112  recexap  8275  div32ap  8313  divsubdirap  8329  divmuldivap  8333  divdivdivap  8334  divmuleqap  8338  divcanap6  8340  dmdcanap  8343  divsubdivap  8349  div2negap  8356  div2subap  8457  mvllmulapd  8459  prodgt0gt0  8467  cju  8577  zneo  9004  infrenegsupex  9239  qreccl  9284  xnpcan  9496  fzosn  9823  modqid  9963  modqm1p1mod0  9989  modqltm1p1mod  9990  modqmul1  9991  modaddmodup  10001  modaddmodlo  10002  modqsubdir  10007  iseqf1olemkle  10098  iseqf1olemklt  10099  seq3f1olemstep  10115  seq3f1oleml  10117  seqfeq3  10126  seq3distr  10127  expineg2  10143  expm1t  10162  expadd  10176  expaddzaplem  10177  expmulzap  10180  sqsubswap  10194  subsq2  10241  binom2sub  10246  binom3  10250  facndiv  10326  bcval5  10350  bcn2p1  10357  bcnm1  10359  2shfti  10444  shftcan2  10448  reim0  10474  imval2  10507  cjreim2  10517  cjdivap  10522  cnrecnv  10523  rennim  10614  resqrexlemnm  10630  remsqsqrt  10644  sqrtdiv  10654  sqrtmsq  10657  sqabsadd  10667  sqabssub  10668  absreim  10680  absdivap  10682  absnid  10685  sqabs  10694  abslt  10700  absle  10701  recvalap  10709  abssub  10713  maxabslemlub  10819  infxrnegsupex  10871  mulcn2  10920  reccn2ap  10921  cjcn2  10924  summodclem3  10988  summodclem2a  10989  summodc  10991  zsumdc  10992  fsum3  10995  fisumss  11000  fsumcl2lem  11006  fsumm1  11024  fsum1p  11026  isummulc2  11034  telfsumo  11074  binomlem  11091  bcxmas  11097  arisum  11106  trireciplem  11108  trirecip  11109  geolim2  11120  georeclim  11121  cvgratnnlemfm  11137  cvgratz  11140  mertenslemi1  11143  efcan  11180  efexp  11186  efzval  11187  efgt0  11188  eftlub  11194  efltim  11202  resinval  11220  recosval  11221  cosmul  11250  cos2t  11255  cos2tsin  11256  cos01bnd  11263  eirraplem  11278  muldvds1  11313  dvdsexp  11354  oexpneg  11369  divalglemqt  11411  divalglemeunn  11413  divalglemeuneg  11415  divalgmod  11419  flodddiv4t2lthalf  11429  gcdid0  11463  gcdaddm  11467  rpmulgcd  11507  sqgcd  11510  algcvg  11522  eucalgcvga  11532  eucalg  11533  dvdslcm  11543  lcmeq0  11545  lcmgcd  11552  qredeu  11571  sqnprm  11609  divgcdodd  11614  sqrt2irrlem  11632  sqpweven  11645  2sqpwodd  11646  divnumden  11666  hashdvds  11689  phimullem  11693  ennnfonelemhf1o  11718  strslssd  11787  topnidg  11915  restopnb  12132  txcnmpt  12223  cnmpt1t  12235  blhalf  12336  xmspropd  12405  mspropd  12406  limcimolemlt  12513  peano3nninf  12785  nninfsel  12797  nninffeq  12800  isomninnlem  12809  cvgcmp2nlemabs  12811  trilpolemlt1  12818