Theorem eqtr3d 2264

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

Syntax hints:   -> wi 4   = wceq 1395

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 1493  ax-gen 1495  ax-4 1556  ax-17 1572  ax-ext 2211

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

This theorem is referenced by:  3eqtr3d  2270  3eqtr3rd  2271  3eqtr3a  2286  opth  4322  eusvnf  4543  f00  5516  f1imacnv  5588  foimacnv  5589  f1ococnv1  5600  funfvdm  5696  fvmptdf  5721  fndmdif  5739  funopsn  5816  acexmidlemph  5993  acexmidlemab  5994  ovmpodf  6135  fvmpopr2d  6140  oprssov  6146  tfrlemisucaccv  6469  tfr1onlemsucaccv  6485  tfrcllemsucaccv  6498  oav2  6607  omv2  6609  fnsnsplitdc  6649  ecopovtrn  6777  ecopovtrng  6780  map0b  6832  en1  6949  ssenen  7008  fidifsnen  7028  dif1en  7037  undifdc  7082  fidcenumlemr  7118  ordiso2  7198  nninfninc  7286  nnnninfeq2  7292  nninfisollemne  7294  finomni  7303  exmidomni  7305  fodjum  7309  exmidaclem  7386  distrnqg  7570  1qec  7571  prarloclemarch2  7602  nnnq0lem1  7629  nqpnq0nq  7636  distrnq0  7642  prarloclemlt  7676  prmuloclemcalc  7748  ltaprg  7802  prplnqu  7803  recexprlem1ssl  7816  recexprlem1ssu  7817  ltmprr  7825  cauappcvgprlemopl  7829  caucvgprlemopl  7852  caucvgprprlemopl  7880  caucvgprprlemexb  7890  prsrlem1  7925  ltsosr  7947  mulgt0sr  7961  recidpipr  8039  recriota  8073  nntopi  8077  axcaucvglemres  8082  addlid  8281  readdcan  8282  muladd11r  8298  add32r  8302  cnegexlem2  8318  cnegex  8320  pncan2  8349  addsubass  8352  subadd23  8354  addsub12  8355  subid  8361  subid1  8362  npncan  8363  nppcan3  8366  subsub  8372  nppcan2  8373  nnncan2  8379  npncan3  8380  pnpcan  8381  negdi  8399  mvlraddd  8506  mvlladdd  8507  pnpncand  8517  subdi  8527  mulsub  8543  mulsub2  8544  eqord1  8626  recexap  8796  div32ap  8835  divsubdirap  8851  divmuldivap  8855  divdivdivap  8856  divmuleqap  8860  divcanap6  8862  dmdcanap  8865  divsubdivap  8871  div2negap  8878  div2subap  8980  mvllmulapd  8985  prodgt0gt0  8994  cju  9104  zneo  9544  infrenegsupex  9785  qreccl  9833  mul2lt0rlt0  9951  xnpcan  10064  fzosn  10406  modqid  10566  modqm1p1mod0  10592  modqltm1p1mod  10593  modqmul1  10594  modaddmodup  10604  modaddmodlo  10605  modqsubdir  10610  iseqf1olemkle  10714  iseqf1olemklt  10715  seq3f1olemstep  10731  seq3f1oleml  10733  seqf1oglem2  10737  seqfeq3  10746  seq3distr  10749  expineg2  10765  expm1t  10784  expadd  10798  expaddzaplem  10799  expmulzap  10802  sqsubswap  10816  subsq2  10864  binom2sub  10870  binom3  10874  facndiv  10956  bcval5  10980  bcn2p1  10987  bcnm1  10989  pfxccatpfx2  11264  2shfti  11337  shftcan2  11341  reim0  11367  imval2  11400  cjreim2  11410  cjdivap  11415  cnrecnv  11416  rennim  11508  resqrexlemnm  11524  remsqsqrt  11538  sqrtdiv  11548  sqrtmsq  11551  sqabsadd  11561  sqabssub  11562  absreim  11574  absdivap  11576  absnid  11579  sqabs  11588  abslt  11594  absle  11595  recvalap  11603  abssub  11607  maxabslemlub  11713  infxrnegsupex  11769  mulcn2  11818  reccn2ap  11819  cjcn2  11822  summodclem3  11886  summodclem2a  11887  summodc  11889  zsumdc  11890  fsum3  11893  fisumss  11898  fsumcl2lem  11904  fsumm1  11922  fsum1p  11924  isummulc2  11932  telfsumo  11972  binomlem  11989  bcxmas  11995  arisum  12004  trireciplem  12006  trirecip  12007  geolim2  12018  georeclim  12019  cvgratnnlemfm  12035  cvgratz  12038  mertenslemi1  12041  clim2divap  12046  prodmodclem3  12081  prodmodclem2a  12082  zproddc  12085  fprodseq  12089  fprodssdc  12096  fprod1p  12105  efcan  12182  efexp  12188  efzval  12189  efgt0  12190  eftlub  12196  efltim  12204  resinval  12221  recosval  12222  cosmul  12251  cos2t  12256  cos2tsin  12257  cos01bnd  12264  cos12dec  12274  eirraplem  12283  muldvds1  12322  dvdsexp  12367  oexpneg  12383  divalglemqt  12425  divalglemeunn  12427  divalglemeuneg  12429  divalgmod  12433  flodddiv4t2lthalf  12445  bitsmod  12462  bitsinv1lem  12467  gcdid0  12496  gcdaddm  12500  dvdsgcdidd  12510  rpmulgcd  12542  sqgcd  12545  algcvg  12565  eucalgcvga  12575  eucalg  12576  dvdslcm  12586  lcmeq0  12588  lcmgcd  12595  qredeu  12614  sqnprm  12653  divgcdodd  12660  sqrt2irrlem  12678  sqpweven  12692  2sqpwodd  12693  divnumden  12713  hashdvds  12738  phimullem  12742  eulerthlemrprm  12746  eulerthlemth  12749  odzdvds  12763  pythagtriplem3  12785  pythagtriplem4  12786  pythagtriplem14  12795  pythagtriplem19  12800  pcpremul  12811  pceulem  12812  pcqdiv  12825  pcaddlem  12857  fldivp1  12866  1arithlem4  12884  4sqlem10  12905  mul4sqlem  12911  4sqlem11  12919  4sqlem15  12923  4sqlem16  12924  4sqlem17  12925  ennnfonelemhf1o  12979  strslssd  13074  ressbas2d  13096  ressinbasd  13102  topnidg  13280  lidrideqd  13409  grpidd  13411  grprida  13415  gsumress  13423  ismndd  13465  grpidd2  13569  grpinvid1  13580  grpinvid2  13581  grppnpcan2  13622  grpnpncan  13623  dfgrp3mlem  13626  grpsubpropd2  13633  mhmid  13647  mhmmnd  13648  mulgsubcl  13668  mulgneg  13672  mulgaddcomlem  13677  mulginvinv  13680  mulgdirlem  13685  mulgdir  13686  mulgass  13691  mulgmodid  13693  grpissubg  13726  eqgcpbl  13760  ghmid  13781  ghmmulg  13788  resghm  13792  invghm  13861  gsumfzmptfidmadd  13871  mgptopng  13887  srgisid  13944  ringidss  13987  ringcom  13989  opprsubgg  14042  unitgrp  14074  1rinv  14086  0unit  14087  rhmdvdsr  14133  lringuplu  14154  subrngpropd  14174  subrgpropd  14211  lmod0vs  14279  lmodvsmmulgdi  14281  lmodvneg1  14288  lmodcom  14291  lmodsubvs  14301  lmodsubdir  14303  lmodpropd  14307  lspsnsub  14379  lspsneq0b  14385  lsppropd  14390  rlmscabas  14418  lidlbas  14436  zringmulg  14556  restopnb  14849  txcnmpt  14941  cnmpt1t  14953  blhalf  15076  xmspropd  15145  mspropd  15146  mpomulcn  15234  ivthreinc  15313  limcimolemlt  15332  dvfre  15378  dveflem  15394  dvef  15395  ply1termlem  15410  plymullem1  15416  sin2kpi  15479  cos2kpi  15480  sin2pim  15481  cos2pim  15482  ptolemy  15492  sincosq2sgn  15495  sincosq3sgn  15496  sincosq4sgn  15497  sinq12gt0  15498  tangtx  15506  sincosq1eq  15507  abssinper  15514  sinkpi  15515  relogeftb  15533  relogoprlem  15536  relogexp  15540  mpodvdsmulf1o  15658  mersenne  15665  perfectlem1  15667  perfectlem2  15668  perfect  15669  lgsval2lem  15683  lgsdir2lem4  15704  lgsdirprm  15707  lgsdilem2  15709  gausslemma2dlem7  15741  lgseisenlem4  15746  lgsquadlem1  15750  lgsquadlem2  15751  lgsquad2lem1  15754  lgsquad2lem2  15755  2sqlem4  15791  2sqlem6  15793  2sqlem8  15796  peano3nninf  16332  nninfsel  16342  nninffeq  16345  isomninnlem  16357  cvgcmp2nlemabs  16359  trilpolemlt1  16368  trirec0xor  16372  ismkvnnlem  16379