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  mgptopng  14312  srgisid  14374  ringidss  14418  ringcom  14420  opprsubgg  14474  unitgrp  14507  1rinv  14519  0unit  14520  rhmdvdsr  14566  lringuplu  14587  subrngpropd  14608  subrgpropd  14645  lmod0vs  14742  lmodvsmmulgdi  14744  lmodvneg1  14751  lmodcom  14754  lmodsubvs  14764  lmodsubdir  14766  lmodpropd  14770  lspsnsub  14842  lspsneq0b  14848  lsppropd  14853  rlmscabas  14881  lidlbas  14899  zringmulg  15017  restopnb  15373  txcnmpt  15465  cnmpt1t  15477  blhalf  15600  xmspropd  15669  mspropd  15670  mpomulcn  15758  ivthreinc  15837  limcimolemlt  15856  dvfre  15902  dveflem  15918  dvef  15919  ply1termlem  15934  plymullem1  15940  sin2kpi  16004  cos2kpi  16005  sin2pim  16006  cos2pim  16007  ptolemy  16017  sincosq2sgn  16020  sincosq3sgn  16021  sincosq4sgn  16022  sinq12gt0  16023  tangtx  16031  sincosq1eq  16032  abssinper  16039  sinkpi  16040  relogeftb  16058  relogoprlem  16062  relogexp  16066  log2tlbndlog2  16181  birthdaylem2  16187  birthdaylem3  16188  pellexlem1  16190  efchtqdvds  16226  ppiqp1le  16228  ppiqltx  16242  mpodvdsmulf1o  16245  ppiqub  16254  chtqub  16257  mersenne  16258  perfectlem1  16260  perfectlem2  16261  perfect  16262  bposlem6  16277  bposlem9  16280  lgsval2lem  16295  lgsdir2lem4  16316  lgsdirprm  16319  lgsdilem2  16321  gausslemma2dlem7  16353  lgseisenlem4  16358  lgsquadlem1  16362  lgsquadlem2  16363  lgsquad2lem1  16366  lgsquad2lem2  16367  2sqlem4  16403  2sqlem6  16405  2sqlem8  16408  clwwlknonel  16839  eupth2fi  16886  dichmul0orlem2  16920  dichmul0orlem3  16921  dichmul0orlem4  16922  peano3nninf  17216  nninfsel  17226  nninffeq  17229  isomninnlem  17245  cvgcmp2nlemabs  17247  trilpolemlt1  17257  trirec0xor  17261  qdiff  17265  ismkvnnlem  17269