Theorem eqtr3d 2231

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 2202	. 2 |- ( ph -> B = A )
3		eqtr3d.2	. 2 |- ( ph -> A = C )
4	2, 3	eqtrd 2229	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 1461  ax-gen 1463  ax-4 1524  ax-17 1540  ax-ext 2178

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

This theorem is referenced by:  3eqtr3d  2237  3eqtr3rd  2238  3eqtr3a  2253  opth  4271  eusvnf  4489  f00  5452  f1imacnv  5524  foimacnv  5525  f1ococnv1  5536  funfvdm  5627  fvmptdf  5652  fndmdif  5670  acexmidlemph  5918  acexmidlemab  5919  ovmpodf  6058  fvmpopr2d  6063  oprssov  6069  tfrlemisucaccv  6392  tfr1onlemsucaccv  6408  tfrcllemsucaccv  6421  oav2  6530  omv2  6532  fnsnsplitdc  6572  ecopovtrn  6700  ecopovtrng  6703  map0b  6755  en1  6867  ssenen  6921  fidifsnen  6940  dif1en  6949  undifdc  6994  fidcenumlemr  7030  ordiso2  7110  nninfninc  7198  nnnninfeq2  7204  nninfisollemne  7206  finomni  7215  exmidomni  7217  fodjum  7221  exmidaclem  7291  distrnqg  7471  1qec  7472  prarloclemarch2  7503  nnnq0lem1  7530  nqpnq0nq  7537  distrnq0  7543  prarloclemlt  7577  prmuloclemcalc  7649  ltaprg  7703  prplnqu  7704  recexprlem1ssl  7717  recexprlem1ssu  7718  ltmprr  7726  cauappcvgprlemopl  7730  caucvgprlemopl  7753  caucvgprprlemopl  7781  caucvgprprlemexb  7791  prsrlem1  7826  ltsosr  7848  mulgt0sr  7862  recidpipr  7940  recriota  7974  nntopi  7978  axcaucvglemres  7983  addlid  8182  readdcan  8183  muladd11r  8199  add32r  8203  cnegexlem2  8219  cnegex  8221  pncan2  8250  addsubass  8253  subadd23  8255  addsub12  8256  subid  8262  subid1  8263  npncan  8264  nppcan3  8267  subsub  8273  nppcan2  8274  nnncan2  8280  npncan3  8281  pnpcan  8282  negdi  8300  mvlraddd  8407  mvlladdd  8408  pnpncand  8418  subdi  8428  mulsub  8444  mulsub2  8445  eqord1  8527  recexap  8697  div32ap  8736  divsubdirap  8752  divmuldivap  8756  divdivdivap  8757  divmuleqap  8761  divcanap6  8763  dmdcanap  8766  divsubdivap  8772  div2negap  8779  div2subap  8881  mvllmulapd  8886  prodgt0gt0  8895  cju  9005  zneo  9444  infrenegsupex  9685  qreccl  9733  mul2lt0rlt0  9851  xnpcan  9964  fzosn  10298  modqid  10458  modqm1p1mod0  10484  modqltm1p1mod  10485  modqmul1  10486  modaddmodup  10496  modaddmodlo  10497  modqsubdir  10502  iseqf1olemkle  10606  iseqf1olemklt  10607  seq3f1olemstep  10623  seq3f1oleml  10625  seqf1oglem2  10629  seqfeq3  10638  seq3distr  10641  expineg2  10657  expm1t  10676  expadd  10690  expaddzaplem  10691  expmulzap  10694  sqsubswap  10708  subsq2  10756  binom2sub  10762  binom3  10766  facndiv  10848  bcval5  10872  bcn2p1  10879  bcnm1  10881  2shfti  11013  shftcan2  11017  reim0  11043  imval2  11076  cjreim2  11086  cjdivap  11091  cnrecnv  11092  rennim  11184  resqrexlemnm  11200  remsqsqrt  11214  sqrtdiv  11224  sqrtmsq  11227  sqabsadd  11237  sqabssub  11238  absreim  11250  absdivap  11252  absnid  11255  sqabs  11264  abslt  11270  absle  11271  recvalap  11279  abssub  11283  maxabslemlub  11389  infxrnegsupex  11445  mulcn2  11494  reccn2ap  11495  cjcn2  11498  summodclem3  11562  summodclem2a  11563  summodc  11565  zsumdc  11566  fsum3  11569  fisumss  11574  fsumcl2lem  11580  fsumm1  11598  fsum1p  11600  isummulc2  11608  telfsumo  11648  binomlem  11665  bcxmas  11671  arisum  11680  trireciplem  11682  trirecip  11683  geolim2  11694  georeclim  11695  cvgratnnlemfm  11711  cvgratz  11714  mertenslemi1  11717  clim2divap  11722  prodmodclem3  11757  prodmodclem2a  11758  zproddc  11761  fprodseq  11765  fprodssdc  11772  fprod1p  11781  efcan  11858  efexp  11864  efzval  11865  efgt0  11866  eftlub  11872  efltim  11880  resinval  11897  recosval  11898  cosmul  11927  cos2t  11932  cos2tsin  11933  cos01bnd  11940  cos12dec  11950  eirraplem  11959  muldvds1  11998  dvdsexp  12043  oexpneg  12059  divalglemqt  12101  divalglemeunn  12103  divalglemeuneg  12105  divalgmod  12109  flodddiv4t2lthalf  12121  bitsmod  12138  bitsinv1lem  12143  gcdid0  12172  gcdaddm  12176  dvdsgcdidd  12186  rpmulgcd  12218  sqgcd  12221  algcvg  12241  eucalgcvga  12251  eucalg  12252  dvdslcm  12262  lcmeq0  12264  lcmgcd  12271  qredeu  12290  sqnprm  12329  divgcdodd  12336  sqrt2irrlem  12354  sqpweven  12368  2sqpwodd  12369  divnumden  12389  hashdvds  12414  phimullem  12418  eulerthlemrprm  12422  eulerthlemth  12425  odzdvds  12439  pythagtriplem3  12461  pythagtriplem4  12462  pythagtriplem14  12471  pythagtriplem19  12476  pcpremul  12487  pceulem  12488  pcqdiv  12501  pcaddlem  12533  fldivp1  12542  1arithlem4  12560  4sqlem10  12581  mul4sqlem  12587  4sqlem11  12595  4sqlem15  12599  4sqlem16  12600  4sqlem17  12601  ennnfonelemhf1o  12655  strslssd  12750  ressbas2d  12771  ressinbasd  12777  topnidg  12954  lidrideqd  13083  grpidd  13085  grprida  13089  gsumress  13097  ismndd  13139  grpidd2  13243  grpinvid1  13254  grpinvid2  13255  grppnpcan2  13296  grpnpncan  13297  dfgrp3mlem  13300  grpsubpropd2  13307  mhmid  13321  mhmmnd  13322  mulgsubcl  13342  mulgneg  13346  mulgaddcomlem  13351  mulginvinv  13354  mulgdirlem  13359  mulgdir  13360  mulgass  13365  mulgmodid  13367  grpissubg  13400  eqgcpbl  13434  ghmid  13455  ghmmulg  13462  resghm  13466  invghm  13535  gsumfzmptfidmadd  13545  mgptopng  13561  srgisid  13618  ringidss  13661  ringcom  13663  opprsubgg  13716  unitgrp  13748  1rinv  13760  0unit  13761  rhmdvdsr  13807  lringuplu  13828  subrngpropd  13848  subrgpropd  13885  lmod0vs  13953  lmodvsmmulgdi  13955  lmodvneg1  13962  lmodcom  13965  lmodsubvs  13975  lmodsubdir  13977  lmodpropd  13981  lspsnsub  14053  lspsneq0b  14059  lsppropd  14064  rlmscabas  14092  lidlbas  14110  zringmulg  14230  restopnb  14501  txcnmpt  14593  cnmpt1t  14605  blhalf  14728  xmspropd  14797  mspropd  14798  mpomulcn  14886  ivthreinc  14965  limcimolemlt  14984  dvfre  15030  dveflem  15046  dvef  15047  ply1termlem  15062  plymullem1  15068  sin2kpi  15131  cos2kpi  15132  sin2pim  15133  cos2pim  15134  ptolemy  15144  sincosq2sgn  15147  sincosq3sgn  15148  sincosq4sgn  15149  sinq12gt0  15150  tangtx  15158  sincosq1eq  15159  abssinper  15166  sinkpi  15167  relogeftb  15185  relogoprlem  15188  relogexp  15192  mpodvdsmulf1o  15310  mersenne  15317  perfectlem1  15319  perfectlem2  15320  perfect  15321  lgsval2lem  15335  lgsdir2lem4  15356  lgsdirprm  15359  lgsdilem2  15361  gausslemma2dlem7  15393  lgseisenlem4  15398  lgsquadlem1  15402  lgsquadlem2  15403  lgsquad2lem1  15406  lgsquad2lem2  15407  2sqlem4  15443  2sqlem6  15445  2sqlem8  15448  peano3nninf  15738  nninfsel  15748  nninffeq  15751  isomninnlem  15761  cvgcmp2nlemabs  15763  trilpolemlt1  15772  trirec0xor  15776  ismkvnnlem  15783