Theorem eqtr3d 2200

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

Syntax hints:   -> wi 4   = wceq 1343

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 1435  ax-gen 1437  ax-4 1498  ax-17 1514  ax-ext 2147

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

This theorem is referenced by:  3eqtr3d  2206  3eqtr3rd  2207  3eqtr3a  2223  opth  4215  eusvnf  4431  f00  5379  f1imacnv  5449  foimacnv  5450  f1ococnv1  5461  funfvdm  5549  fvmptdf  5573  fndmdif  5590  acexmidlemph  5835  acexmidlemab  5836  ovmpodf  5973  oprssov  5983  tfrlemisucaccv  6293  tfr1onlemsucaccv  6309  tfrcllemsucaccv  6322  oav2  6431  omv2  6433  fnsnsplitdc  6473  ecopovtrn  6598  ecopovtrng  6601  map0b  6653  en1  6765  ssenen  6817  fidifsnen  6836  dif1en  6845  undifdc  6889  fidcenumlemr  6920  ordiso2  7000  nnnninfeq2  7093  nninfisollemne  7095  finomni  7104  exmidomni  7106  fodjum  7110  exmidaclem  7164  distrnqg  7328  1qec  7329  prarloclemarch2  7360  nnnq0lem1  7387  nqpnq0nq  7394  distrnq0  7400  prarloclemlt  7434  prmuloclemcalc  7506  ltaprg  7560  prplnqu  7561  recexprlem1ssl  7574  recexprlem1ssu  7575  ltmprr  7583  cauappcvgprlemopl  7587  caucvgprlemopl  7610  caucvgprprlemopl  7638  caucvgprprlemexb  7648  prsrlem1  7683  ltsosr  7705  mulgt0sr  7719  recidpipr  7797  recriota  7831  nntopi  7835  axcaucvglemres  7840  addid2  8037  readdcan  8038  muladd11r  8054  add32r  8058  cnegexlem2  8074  cnegex  8076  pncan2  8105  addsubass  8108  subadd23  8110  addsub12  8111  subid  8117  subid1  8118  npncan  8119  nppcan3  8122  subsub  8128  nppcan2  8129  nnncan2  8135  npncan3  8136  pnpcan  8137  negdi  8155  mvlraddd  8262  mvlladdd  8263  pnpncand  8273  subdi  8283  mulsub  8299  mulsub2  8300  eqord1  8381  recexap  8550  div32ap  8588  divsubdirap  8604  divmuldivap  8608  divdivdivap  8609  divmuleqap  8613  divcanap6  8615  dmdcanap  8618  divsubdivap  8624  div2negap  8631  div2subap  8733  mvllmulapd  8738  prodgt0gt0  8746  cju  8856  zneo  9292  infrenegsupex  9532  qreccl  9580  mul2lt0rlt0  9695  xnpcan  9808  fzosn  10140  modqid  10284  modqm1p1mod0  10310  modqltm1p1mod  10311  modqmul1  10312  modaddmodup  10322  modaddmodlo  10323  modqsubdir  10328  iseqf1olemkle  10419  iseqf1olemklt  10420  seq3f1olemstep  10436  seq3f1oleml  10438  seqfeq3  10447  seq3distr  10448  expineg2  10464  expm1t  10483  expadd  10497  expaddzaplem  10498  expmulzap  10501  sqsubswap  10515  subsq2  10562  binom2sub  10568  binom3  10572  facndiv  10652  bcval5  10676  bcn2p1  10683  bcnm1  10685  2shfti  10773  shftcan2  10777  reim0  10803  imval2  10836  cjreim2  10846  cjdivap  10851  cnrecnv  10852  rennim  10944  resqrexlemnm  10960  remsqsqrt  10974  sqrtdiv  10984  sqrtmsq  10987  sqabsadd  10997  sqabssub  10998  absreim  11010  absdivap  11012  absnid  11015  sqabs  11024  abslt  11030  absle  11031  recvalap  11039  abssub  11043  maxabslemlub  11149  infxrnegsupex  11204  mulcn2  11253  reccn2ap  11254  cjcn2  11257  summodclem3  11321  summodclem2a  11322  summodc  11324  zsumdc  11325  fsum3  11328  fisumss  11333  fsumcl2lem  11339  fsumm1  11357  fsum1p  11359  isummulc2  11367  telfsumo  11407  binomlem  11424  bcxmas  11430  arisum  11439  trireciplem  11441  trirecip  11442  geolim2  11453  georeclim  11454  cvgratnnlemfm  11470  cvgratz  11473  mertenslemi1  11476  clim2divap  11481  prodmodclem3  11516  prodmodclem2a  11517  zproddc  11520  fprodseq  11524  fprodssdc  11531  fprod1p  11540  efcan  11617  efexp  11623  efzval  11624  efgt0  11625  eftlub  11631  efltim  11639  resinval  11656  recosval  11657  cosmul  11686  cos2t  11691  cos2tsin  11692  cos01bnd  11699  cos12dec  11708  eirraplem  11717  muldvds1  11756  dvdsexp  11799  oexpneg  11814  divalglemqt  11856  divalglemeunn  11858  divalglemeuneg  11860  divalgmod  11864  flodddiv4t2lthalf  11874  gcdid0  11913  gcdaddm  11917  dvdsgcdidd  11927  rpmulgcd  11959  sqgcd  11962  algcvg  11980  eucalgcvga  11990  eucalg  11991  dvdslcm  12001  lcmeq0  12003  lcmgcd  12010  qredeu  12029  sqnprm  12068  divgcdodd  12075  sqrt2irrlem  12093  sqpweven  12107  2sqpwodd  12108  divnumden  12128  hashdvds  12153  phimullem  12157  eulerthlemrprm  12161  eulerthlemth  12164  odzdvds  12177  pythagtriplem3  12199  pythagtriplem4  12200  pythagtriplem14  12209  pythagtriplem19  12214  pcpremul  12225  pceulem  12226  pcqdiv  12239  pcaddlem  12270  fldivp1  12278  1arithlem4  12296  4sqlem10  12317  mul4sqlem  12323  ennnfonelemhf1o  12346  strslssd  12440  topnidg  12569  lidrideqd  12612  grpidd  12614  grpridd  12618  restopnb  12821  txcnmpt  12913  cnmpt1t  12925  blhalf  13048  xmspropd  13117  mspropd  13118  limcimolemlt  13273  dvfre  13314  dveflem  13327  dvef  13328  sin2kpi  13372  cos2kpi  13373  sin2pim  13374  cos2pim  13375  ptolemy  13385  sincosq2sgn  13388  sincosq3sgn  13389  sincosq4sgn  13390  sinq12gt0  13391  tangtx  13399  sincosq1eq  13400  abssinper  13407  sinkpi  13408  relogeftb  13426  relogoprlem  13429  relogexp  13433  lgsval2lem  13551  lgsdir2lem4  13572  lgsdirprm  13575  lgsdilem2  13577  2sqlem4  13594  2sqlem6  13596  2sqlem8  13599  peano3nninf  13887  nninfsel  13897  nninffeq  13900  isomninnlem  13909  cvgcmp2nlemabs  13911  trilpolemlt1  13920  trirec0xor  13924  ismkvnnlem  13931