Theorem eqtr3d 2273

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

This proof depends on syntax axioms:   -> wi 4   = wceq 1402

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231

This theorem is used by:  3eqtr3d  2279  3eqtr3rd  2280  3eqtr3a  2295  opth  4377  eusvnf  4599  f00  5584  f1imacnv  5656  foimacnv  5657  f1ococnv1  5668  funfvdm  5766  fvmptdf  5793  fndmdif  5814  funopsn  5891  acexmidlemph  6078  acexmidlemab  6079  ovmpodf  6220  fvmpopr2d  6225  oprssov  6231  tfrlemisucaccv  6596  tfr1onlemsucaccv  6612  tfrcllemsucaccv  6625  oav2  6736  omv2  6738  fnsnsplitdc  6778  ecopovtrn  6906  ecopovtrng  6909  map0b  6968  en1  7086  ssenen  7152  fidifsnen  7172  dif1en  7183  undifdc  7231  fidcenumlemr  7272  ordiso2  7376  nninfninc  7464  nnnninfeq2  7470  nninfisollemne  7472  finomni  7481  exmidomni  7483  fodjum  7487  exmidaclem  7565  distrnqg  7755  1qec  7756  prarloclemarch2  7787  nnnq0lem1  7814  nqpnq0nq  7821  distrnq0  7827  prarloclemlt  7861  prmuloclemcalc  7933  ltaprg  7987  prplnqu  7988  recexprlem1ssl  8001  recexprlem1ssu  8002  ltmprr  8010  cauappcvgprlemopl  8014  caucvgprlemopl  8037  caucvgprprlemopl  8065  caucvgprprlemexb  8075  prsrlem1  8110  ltsosr  8132  mulgt0sr  8146  recidpipr  8224  recriota  8258  nntopi  8262  axcaucvglemres  8267  addlid  8467  readdcan  8468  muladd11r  8484  add32r  8488  cnegexlem2  8504  cnegex  8506  pncan2  8535  addsubass  8538  subadd23  8540  addsub12  8541  subid  8547  subid1  8548  npncan  8549  nppcan3  8552  subsub  8558  nppcan2  8559  nnncan2  8565  npncan3  8566  pnpcan  8567  negdi  8585  mvlraddd  8692  mvlladdd  8693  pnpncand  8703  subdi  8714  mulsub  8730  mulsub2  8731  eqord1  8813  recexap  8984  div32ap  9025  divsubdirap  9041  divmuldivap  9045  divdivdivap  9046  divmuleqap  9050  divcanap6  9052  dmdcanap  9055  divsubdivap  9061  div2negap  9068  div2subap  9170  mvllmulapd  9175  prodgt0gt0  9184  cju  9294  zneo  9752  infrenegsupex  10004  qreccl  10052  mul2lt0rlt0  10171  xnpcan  10285  fzosn  10634  modqid  10801  modqm1p1mod0  10827  modqltm1p1mod  10828  modqmul1  10829  modaddmodup  10839  modaddmodlo  10840  modqsubdir  10845  iseqf1olemkle  10949  iseqf1olemklt  10950  seq3f1olemstep  10966  seq3f1oleml  10968  seqf1oglem2  10972  seqfeq3  10981  seq3distr  10984  expineg2  11000  expm1t  11019  expadd  11033  expaddzaplem  11034  expmulzap  11037  sqsubswap  11051  subsq2  11099  binom2sub  11105  binom3  11109  resq01  11110  facndiv  11193  bcval5  11217  bcn2p1  11225  bcnm1  11227  hashpwfi  11285  hashfibclem  11298  pfxccatpfx2  11525  2shfti  11612  shftcan2  11616  reim0  11642  imval2  11675  cjreim2  11686  cjdivap  11691  cnrecnv  11692  rennim  11784  resqrexlemnm  11800  remsqsqrt  11814  sqrtdiv  11824  sqrtmsq  11827  sqabsadd  11837  sqabssub  11838  absreim  11850  absdivap  11852  absnid  11855  sqabs  11865  abslt  11871  absle  11872  recvalap  11880  abssub  11884  maxabslemlub  11990  infxrnegsupex  12048  mulcn2  12097  reccn2ap  12098  cjcn2  12101  summodclem3  12166  summodclem2a  12167  summodc  12169  zsumdc  12170  fsum3  12173  fisumss  12178  fsumcl2lem  12184  fsumm1  12202  fsum1p  12204  isummulc2  12212  telfsumo  12252  binomlem  12269  bcxmas  12275  arisum  12284  trireciplem  12286  trirecip  12287  geolim2  12298  georeclim  12299  cvgratnnlemfm  12315  cvgratz  12318  mertenslemi1  12321  clim2divap  12326  prodmodclem3  12361  prodmodclem2a  12362  zproddc  12365  fprodseq  12369  fprodssdc  12376  fprod1p  12385  efcan  12462  efexp  12468  efzval  12469  efgt0  12470  eftlub  12476  efltim  12484  resinval  12501  recosval  12502  cosmul  12531  cos2t  12536  cos2tsin  12537  cos01bnd  12544  cos12dec  12554  eirraplem  12563  muldvds1  12602  dvdsexp  12647  oexpneg  12663  divalglemqt  12705  divalglemeunn  12707  divalglemeuneg  12709  divalgmod  12713  flodddiv4t2lthalf  12725  bitsmod  12742  bitsinv1lem  12747  gcdid0  12776  gcdaddm  12780  dvdsgcdidd  12790  rpmulgcd  12822  sqgcd  12825  algcvg  12845  eucalgcvga  12855  eucalg  12856  dvdslcm  12866  lcmeq0  12868  lcmgcd  12875  qredeu  12894  sqnprm  12934  divgcdodd  12941  sqrt2irrlem  12959  sqpweven  12974  2sqpwodd  12975  divnumden  12995  hashdvds  13022  phimullem  13026  eulerthlemrprm  13030  eulerthlemth  13033  odzdvds  13047  pythagtriplem3  13069  pythagtriplem4  13070  pythagtriplem14  13079  pythagtriplem19  13084  pcpremul  13095  pceulem  13096  pcqdiv  13109  pcaddlem  13141  fldivp1  13150  1arithlem4  13168  4sqlem10  13189  mul4sqlem  13195  4sqlem11  13203  4sqlem15  13207  4sqlem16  13208  4sqlem17  13209  ballotfilemfc0  13284  ballotfilemfcc  13285  ballotfilemic  13302  ballotfilem1c  13303  ballotfilemfrceq  13324  ballotfilemrinv0  13328  ennnfonelemhf1o  13356  strslssd  13451  ressbas2d  13475  ressinbasd  13481  topnidg  13659  lidrideqd  13754  grpidd  13756  grprida  13760  gzsumress  13765  ismndd  13803  grpidd2  13899  grpinvid1  13910  grpinvid2  13911  grppnpcan2  13952  grpnpncan  13953  dfgrp3mlem  13956  grpsubpropd2  13963  mhmid  13971  mhmmnd  13972  mulgsubcl  13992  mulgneg  13996  mulgaddcomlem  14001  mulginvinv  14004  mulgdirlem  14009  mulgdir  14010  mulgass  14015  mulgmodid  14017  grpissubg  14050  eqgcpbl  14084  ghmid  14105  ghmmulg  14112  resghm  14116  cntrsubgnsg  14169  invghm  14217  gsum0cmn  14238  gsumresfi  14254  mgptopng  14319  srgisid  14381  ringidss  14425  ringcom  14427  opprsubgg  14481  unitgrp  14514  1rinv  14526  0unit  14527  rhmdvdsr  14573  lringuplu  14594  subrngpropd  14615  subrgpropd  14652  lmod0vs  14749  lmodvsmmulgdi  14751  lmodvneg1  14758  lmodcom  14761  lmodsubvs  14771  lmodsubdir  14773  lmodpropd  14777  lspsnsub  14849  lspsneq0b  14855  lsppropd  14860  rlmscabas  14888  lidlbas  14906  zringmulg  15024  restopnb  15381  txcnmpt  15473  cnmpt1t  15485  blhalf  15608  xmspropd  15677  mspropd  15678  mpomulcn  15766  ivthreinc  15845  limcimolemlt  15864  dvfre  15910  dveflem  15926  dvef  15927  ply1termlem  15942  plymullem1  15948  sin2kpi  16012  cos2kpi  16013  sin2pim  16014  cos2pim  16015  ptolemy  16025  sincosq2sgn  16028  sincosq3sgn  16029  sincosq4sgn  16030  sinq12gt0  16031  tangtx  16039  sincosq1eq  16040  abssinper  16047  sinkpi  16048  sineq0re  16050  root1idef  16058  relogeftb  16068  relogoprlem  16072  relogexp  16076  rpcxpmul2z  16122  log2tlbndlog2  16194  birthdaylem2  16200  birthdaylem3  16201  pellexlem1  16203  efchtqdvds  16239  ppiqp1le  16241  ppiqltx  16255  mpodvdsmulf1o  16258  ppiqub  16267  chtqub  16270  mersenne  16271  perfectlem1  16273  perfectlem2  16274  perfect  16275  bposlem6  16290  bposlem9  16293  lgsval2lem  16308  lgsdir2lem4  16329  lgsdirprm  16332  lgsdilem2  16334  gausslemma2dlem7  16366  lgseisenlem4  16371  lgsquadlem1  16375  lgsquadlem2  16376  lgsquad2lem1  16379  lgsquad2lem2  16380  2sqlem4  16416  2sqlem6  16418  2sqlem8  16421  clwwlknonel  16852  eupth2fi  16899  dichmul0orlem2  16933  dichmul0orlem3  16934  dichmul0orlem4  16935  peano3nninf  17229  nninfsel  17239  nninffeq  17242  isomninnlem  17258  cvgcmp2nlemabs  17260  trilpolemlt1  17270  trirec0xor  17274  qdiff  17278  ismkvnnlem  17282