Theorem eqtr3d 2228

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

Syntax hints:   -> wi 4   = wceq 1364

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 1458  ax-gen 1460  ax-4 1521  ax-17 1537  ax-ext 2175

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

This theorem is referenced by:  3eqtr3d  2234  3eqtr3rd  2235  3eqtr3a  2250  opth  4267  eusvnf  4485  f00  5446  f1imacnv  5518  foimacnv  5519  f1ococnv1  5530  funfvdm  5621  fvmptdf  5646  fndmdif  5664  acexmidlemph  5912  acexmidlemab  5913  ovmpodf  6051  fvmpopr2d  6056  oprssov  6062  tfrlemisucaccv  6380  tfr1onlemsucaccv  6396  tfrcllemsucaccv  6409  oav2  6518  omv2  6520  fnsnsplitdc  6560  ecopovtrn  6688  ecopovtrng  6691  map0b  6743  en1  6855  ssenen  6909  fidifsnen  6928  dif1en  6937  undifdc  6982  fidcenumlemr  7016  ordiso2  7096  nninfninc  7184  nnnninfeq2  7190  nninfisollemne  7192  finomni  7201  exmidomni  7203  fodjum  7207  exmidaclem  7270  distrnqg  7449  1qec  7450  prarloclemarch2  7481  nnnq0lem1  7508  nqpnq0nq  7515  distrnq0  7521  prarloclemlt  7555  prmuloclemcalc  7627  ltaprg  7681  prplnqu  7682  recexprlem1ssl  7695  recexprlem1ssu  7696  ltmprr  7704  cauappcvgprlemopl  7708  caucvgprlemopl  7731  caucvgprprlemopl  7759  caucvgprprlemexb  7769  prsrlem1  7804  ltsosr  7826  mulgt0sr  7840  recidpipr  7918  recriota  7952  nntopi  7956  axcaucvglemres  7961  addlid  8160  readdcan  8161  muladd11r  8177  add32r  8181  cnegexlem2  8197  cnegex  8199  pncan2  8228  addsubass  8231  subadd23  8233  addsub12  8234  subid  8240  subid1  8241  npncan  8242  nppcan3  8245  subsub  8251  nppcan2  8252  nnncan2  8258  npncan3  8259  pnpcan  8260  negdi  8278  mvlraddd  8385  mvlladdd  8386  pnpncand  8396  subdi  8406  mulsub  8422  mulsub2  8423  eqord1  8504  recexap  8674  div32ap  8713  divsubdirap  8729  divmuldivap  8733  divdivdivap  8734  divmuleqap  8738  divcanap6  8740  dmdcanap  8743  divsubdivap  8749  div2negap  8756  div2subap  8858  mvllmulapd  8863  prodgt0gt0  8872  cju  8982  zneo  9421  infrenegsupex  9662  qreccl  9710  mul2lt0rlt0  9828  xnpcan  9941  fzosn  10275  modqid  10423  modqm1p1mod0  10449  modqltm1p1mod  10450  modqmul1  10451  modaddmodup  10461  modaddmodlo  10462  modqsubdir  10467  iseqf1olemkle  10571  iseqf1olemklt  10572  seq3f1olemstep  10588  seq3f1oleml  10590  seqf1oglem2  10594  seqfeq3  10603  seq3distr  10606  expineg2  10622  expm1t  10641  expadd  10655  expaddzaplem  10656  expmulzap  10659  sqsubswap  10673  subsq2  10721  binom2sub  10727  binom3  10731  facndiv  10813  bcval5  10837  bcn2p1  10844  bcnm1  10846  2shfti  10978  shftcan2  10982  reim0  11008  imval2  11041  cjreim2  11051  cjdivap  11056  cnrecnv  11057  rennim  11149  resqrexlemnm  11165  remsqsqrt  11179  sqrtdiv  11189  sqrtmsq  11192  sqabsadd  11202  sqabssub  11203  absreim  11215  absdivap  11217  absnid  11220  sqabs  11229  abslt  11235  absle  11236  recvalap  11244  abssub  11248  maxabslemlub  11354  infxrnegsupex  11409  mulcn2  11458  reccn2ap  11459  cjcn2  11462  summodclem3  11526  summodclem2a  11527  summodc  11529  zsumdc  11530  fsum3  11533  fisumss  11538  fsumcl2lem  11544  fsumm1  11562  fsum1p  11564  isummulc2  11572  telfsumo  11612  binomlem  11629  bcxmas  11635  arisum  11644  trireciplem  11646  trirecip  11647  geolim2  11658  georeclim  11659  cvgratnnlemfm  11675  cvgratz  11678  mertenslemi1  11681  clim2divap  11686  prodmodclem3  11721  prodmodclem2a  11722  zproddc  11725  fprodseq  11729  fprodssdc  11736  fprod1p  11745  efcan  11822  efexp  11828  efzval  11829  efgt0  11830  eftlub  11836  efltim  11844  resinval  11861  recosval  11862  cosmul  11891  cos2t  11896  cos2tsin  11897  cos01bnd  11904  cos12dec  11914  eirraplem  11923  muldvds1  11962  dvdsexp  12006  oexpneg  12021  divalglemqt  12063  divalglemeunn  12065  divalglemeuneg  12067  divalgmod  12071  flodddiv4t2lthalf  12081  gcdid0  12120  gcdaddm  12124  dvdsgcdidd  12134  rpmulgcd  12166  sqgcd  12169  algcvg  12189  eucalgcvga  12199  eucalg  12200  dvdslcm  12210  lcmeq0  12212  lcmgcd  12219  qredeu  12238  sqnprm  12277  divgcdodd  12284  sqrt2irrlem  12302  sqpweven  12316  2sqpwodd  12317  divnumden  12337  hashdvds  12362  phimullem  12366  eulerthlemrprm  12370  eulerthlemth  12373  odzdvds  12386  pythagtriplem3  12408  pythagtriplem4  12409  pythagtriplem14  12418  pythagtriplem19  12423  pcpremul  12434  pceulem  12435  pcqdiv  12448  pcaddlem  12480  fldivp1  12489  1arithlem4  12507  4sqlem10  12528  mul4sqlem  12534  4sqlem11  12542  4sqlem15  12546  4sqlem16  12547  4sqlem17  12548  ennnfonelemhf1o  12573  strslssd  12668  ressbas2d  12689  ressinbasd  12695  topnidg  12866  lidrideqd  12967  grpidd  12969  grprida  12973  gsumress  12981  ismndd  13021  grpidd2  13116  grpinvid1  13127  grpinvid2  13128  grppnpcan2  13169  grpnpncan  13170  dfgrp3mlem  13173  grpsubpropd2  13180  mhmid  13188  mhmmnd  13189  mulgsubcl  13209  mulgneg  13213  mulgaddcomlem  13218  mulginvinv  13221  mulgdirlem  13226  mulgdir  13227  mulgass  13232  mulgmodid  13234  grpissubg  13267  eqgcpbl  13301  ghmid  13322  ghmmulg  13329  resghm  13333  invghm  13402  gsumfzmptfidmadd  13412  mgptopng  13428  srgisid  13485  ringidss  13528  ringcom  13530  opprsubgg  13583  unitgrp  13615  1rinv  13627  0unit  13628  rhmdvdsr  13674  lringuplu  13695  subrngpropd  13715  subrgpropd  13752  lmod0vs  13820  lmodvsmmulgdi  13822  lmodvneg1  13829  lmodcom  13832  lmodsubvs  13842  lmodsubdir  13844  lmodpropd  13848  lspsnsub  13920  lspsneq0b  13926  lsppropd  13931  rlmscabas  13959  lidlbas  13977  zringmulg  14097  restopnb  14360  txcnmpt  14452  cnmpt1t  14464  blhalf  14587  xmspropd  14656  mspropd  14657  mpomulcn  14745  ivthreinc  14824  limcimolemlt  14843  dvfre  14889  dveflem  14905  dvef  14906  ply1termlem  14921  plymullem1  14927  sin2kpi  14987  cos2kpi  14988  sin2pim  14989  cos2pim  14990  ptolemy  15000  sincosq2sgn  15003  sincosq3sgn  15004  sincosq4sgn  15005  sinq12gt0  15006  tangtx  15014  sincosq1eq  15015  abssinper  15022  sinkpi  15023  relogeftb  15041  relogoprlem  15044  relogexp  15048  lgsval2lem  15167  lgsdir2lem4  15188  lgsdirprm  15191  lgsdilem2  15193  gausslemma2dlem7  15225  lgseisenlem4  15230  lgsquadlem1  15234  lgsquadlem2  15235  lgsquad2lem1  15238  lgsquad2lem2  15239  2sqlem4  15275  2sqlem6  15277  2sqlem8  15280  peano3nninf  15567  nninfsel  15577  nninffeq  15580  isomninnlem  15590  cvgcmp2nlemabs  15592  trilpolemlt1  15601  trirec0xor  15605  ismkvnnlem  15612