Theorem eqtr3d 2240

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

Syntax hints:   -> wi 4   = wceq 1373

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 1470  ax-gen 1472  ax-4 1533  ax-17 1549  ax-ext 2187

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

This theorem is referenced by:  3eqtr3d  2246  3eqtr3rd  2247  3eqtr3a  2262  opth  4281  eusvnf  4500  f00  5467  f1imacnv  5539  foimacnv  5540  f1ococnv1  5551  funfvdm  5642  fvmptdf  5667  fndmdif  5685  funopsn  5762  acexmidlemph  5937  acexmidlemab  5938  ovmpodf  6077  fvmpopr2d  6082  oprssov  6088  tfrlemisucaccv  6411  tfr1onlemsucaccv  6427  tfrcllemsucaccv  6440  oav2  6549  omv2  6551  fnsnsplitdc  6591  ecopovtrn  6719  ecopovtrng  6722  map0b  6774  en1  6891  ssenen  6948  fidifsnen  6967  dif1en  6976  undifdc  7021  fidcenumlemr  7057  ordiso2  7137  nninfninc  7225  nnnninfeq2  7231  nninfisollemne  7233  finomni  7242  exmidomni  7244  fodjum  7248  exmidaclem  7320  distrnqg  7500  1qec  7501  prarloclemarch2  7532  nnnq0lem1  7559  nqpnq0nq  7566  distrnq0  7572  prarloclemlt  7606  prmuloclemcalc  7678  ltaprg  7732  prplnqu  7733  recexprlem1ssl  7746  recexprlem1ssu  7747  ltmprr  7755  cauappcvgprlemopl  7759  caucvgprlemopl  7782  caucvgprprlemopl  7810  caucvgprprlemexb  7820  prsrlem1  7855  ltsosr  7877  mulgt0sr  7891  recidpipr  7969  recriota  8003  nntopi  8007  axcaucvglemres  8012  addlid  8211  readdcan  8212  muladd11r  8228  add32r  8232  cnegexlem2  8248  cnegex  8250  pncan2  8279  addsubass  8282  subadd23  8284  addsub12  8285  subid  8291  subid1  8292  npncan  8293  nppcan3  8296  subsub  8302  nppcan2  8303  nnncan2  8309  npncan3  8310  pnpcan  8311  negdi  8329  mvlraddd  8436  mvlladdd  8437  pnpncand  8447  subdi  8457  mulsub  8473  mulsub2  8474  eqord1  8556  recexap  8726  div32ap  8765  divsubdirap  8781  divmuldivap  8785  divdivdivap  8786  divmuleqap  8790  divcanap6  8792  dmdcanap  8795  divsubdivap  8801  div2negap  8808  div2subap  8910  mvllmulapd  8915  prodgt0gt0  8924  cju  9034  zneo  9474  infrenegsupex  9715  qreccl  9763  mul2lt0rlt0  9881  xnpcan  9994  fzosn  10334  modqid  10494  modqm1p1mod0  10520  modqltm1p1mod  10521  modqmul1  10522  modaddmodup  10532  modaddmodlo  10533  modqsubdir  10538  iseqf1olemkle  10642  iseqf1olemklt  10643  seq3f1olemstep  10659  seq3f1oleml  10661  seqf1oglem2  10665  seqfeq3  10674  seq3distr  10677  expineg2  10693  expm1t  10712  expadd  10726  expaddzaplem  10727  expmulzap  10730  sqsubswap  10744  subsq2  10792  binom2sub  10798  binom3  10802  facndiv  10884  bcval5  10908  bcn2p1  10915  bcnm1  10917  2shfti  11142  shftcan2  11146  reim0  11172  imval2  11205  cjreim2  11215  cjdivap  11220  cnrecnv  11221  rennim  11313  resqrexlemnm  11329  remsqsqrt  11343  sqrtdiv  11353  sqrtmsq  11356  sqabsadd  11366  sqabssub  11367  absreim  11379  absdivap  11381  absnid  11384  sqabs  11393  abslt  11399  absle  11400  recvalap  11408  abssub  11412  maxabslemlub  11518  infxrnegsupex  11574  mulcn2  11623  reccn2ap  11624  cjcn2  11627  summodclem3  11691  summodclem2a  11692  summodc  11694  zsumdc  11695  fsum3  11698  fisumss  11703  fsumcl2lem  11709  fsumm1  11727  fsum1p  11729  isummulc2  11737  telfsumo  11777  binomlem  11794  bcxmas  11800  arisum  11809  trireciplem  11811  trirecip  11812  geolim2  11823  georeclim  11824  cvgratnnlemfm  11840  cvgratz  11843  mertenslemi1  11846  clim2divap  11851  prodmodclem3  11886  prodmodclem2a  11887  zproddc  11890  fprodseq  11894  fprodssdc  11901  fprod1p  11910  efcan  11987  efexp  11993  efzval  11994  efgt0  11995  eftlub  12001  efltim  12009  resinval  12026  recosval  12027  cosmul  12056  cos2t  12061  cos2tsin  12062  cos01bnd  12069  cos12dec  12079  eirraplem  12088  muldvds1  12127  dvdsexp  12172  oexpneg  12188  divalglemqt  12230  divalglemeunn  12232  divalglemeuneg  12234  divalgmod  12238  flodddiv4t2lthalf  12250  bitsmod  12267  bitsinv1lem  12272  gcdid0  12301  gcdaddm  12305  dvdsgcdidd  12315  rpmulgcd  12347  sqgcd  12350  algcvg  12370  eucalgcvga  12380  eucalg  12381  dvdslcm  12391  lcmeq0  12393  lcmgcd  12400  qredeu  12419  sqnprm  12458  divgcdodd  12465  sqrt2irrlem  12483  sqpweven  12497  2sqpwodd  12498  divnumden  12518  hashdvds  12543  phimullem  12547  eulerthlemrprm  12551  eulerthlemth  12554  odzdvds  12568  pythagtriplem3  12590  pythagtriplem4  12591  pythagtriplem14  12600  pythagtriplem19  12605  pcpremul  12616  pceulem  12617  pcqdiv  12630  pcaddlem  12662  fldivp1  12671  1arithlem4  12689  4sqlem10  12710  mul4sqlem  12716  4sqlem11  12724  4sqlem15  12728  4sqlem16  12729  4sqlem17  12730  ennnfonelemhf1o  12784  strslssd  12879  ressbas2d  12900  ressinbasd  12906  topnidg  13084  lidrideqd  13213  grpidd  13215  grprida  13219  gsumress  13227  ismndd  13269  grpidd2  13373  grpinvid1  13384  grpinvid2  13385  grppnpcan2  13426  grpnpncan  13427  dfgrp3mlem  13430  grpsubpropd2  13437  mhmid  13451  mhmmnd  13452  mulgsubcl  13472  mulgneg  13476  mulgaddcomlem  13481  mulginvinv  13484  mulgdirlem  13489  mulgdir  13490  mulgass  13495  mulgmodid  13497  grpissubg  13530  eqgcpbl  13564  ghmid  13585  ghmmulg  13592  resghm  13596  invghm  13665  gsumfzmptfidmadd  13675  mgptopng  13691  srgisid  13748  ringidss  13791  ringcom  13793  opprsubgg  13846  unitgrp  13878  1rinv  13890  0unit  13891  rhmdvdsr  13937  lringuplu  13958  subrngpropd  13978  subrgpropd  14015  lmod0vs  14083  lmodvsmmulgdi  14085  lmodvneg1  14092  lmodcom  14095  lmodsubvs  14105  lmodsubdir  14107  lmodpropd  14111  lspsnsub  14183  lspsneq0b  14189  lsppropd  14194  rlmscabas  14222  lidlbas  14240  zringmulg  14360  restopnb  14653  txcnmpt  14745  cnmpt1t  14757  blhalf  14880  xmspropd  14949  mspropd  14950  mpomulcn  15038  ivthreinc  15117  limcimolemlt  15136  dvfre  15182  dveflem  15198  dvef  15199  ply1termlem  15214  plymullem1  15220  sin2kpi  15283  cos2kpi  15284  sin2pim  15285  cos2pim  15286  ptolemy  15296  sincosq2sgn  15299  sincosq3sgn  15300  sincosq4sgn  15301  sinq12gt0  15302  tangtx  15310  sincosq1eq  15311  abssinper  15318  sinkpi  15319  relogeftb  15337  relogoprlem  15340  relogexp  15344  mpodvdsmulf1o  15462  mersenne  15469  perfectlem1  15471  perfectlem2  15472  perfect  15473  lgsval2lem  15487  lgsdir2lem4  15508  lgsdirprm  15511  lgsdilem2  15513  gausslemma2dlem7  15545  lgseisenlem4  15550  lgsquadlem1  15554  lgsquadlem2  15555  lgsquad2lem1  15558  lgsquad2lem2  15559  2sqlem4  15595  2sqlem6  15597  2sqlem8  15600  peano3nninf  15944  nninfsel  15954  nninffeq  15957  isomninnlem  15969  cvgcmp2nlemabs  15971  trilpolemlt1  15980  trirec0xor  15984  ismkvnnlem  15991