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 )

Syntax hints:   -> wi 4   = wceq 1402

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 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

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

This theorem is referenced by:  3eqtr3d  2279  3eqtr3rd  2280  3eqtr3a  2295  opth  4372  eusvnf  4594  f00  5579  f1imacnv  5651  foimacnv  5652  f1ococnv1  5663  funfvdm  5760  fvmptdf  5787  fndmdif  5805  funopsn  5882  acexmidlemph  6068  acexmidlemab  6069  ovmpodf  6210  fvmpopr2d  6215  oprssov  6221  tfrlemisucaccv  6586  tfr1onlemsucaccv  6602  tfrcllemsucaccv  6615  oav2  6726  omv2  6728  fnsnsplitdc  6768  ecopovtrn  6896  ecopovtrng  6899  map0b  6958  en1  7076  ssenen  7142  fidifsnen  7162  dif1en  7173  undifdc  7221  fidcenumlemr  7262  ordiso2  7365  nninfninc  7453  nnnninfeq2  7459  nninfisollemne  7461  finomni  7470  exmidomni  7472  fodjum  7476  exmidaclem  7554  distrnqg  7744  1qec  7745  prarloclemarch2  7776  nnnq0lem1  7803  nqpnq0nq  7810  distrnq0  7816  prarloclemlt  7850  prmuloclemcalc  7922  ltaprg  7976  prplnqu  7977  recexprlem1ssl  7990  recexprlem1ssu  7991  ltmprr  7999  cauappcvgprlemopl  8003  caucvgprlemopl  8026  caucvgprprlemopl  8054  caucvgprprlemexb  8064  prsrlem1  8099  ltsosr  8121  mulgt0sr  8135  recidpipr  8213  recriota  8247  nntopi  8251  axcaucvglemres  8256  addlid  8455  readdcan  8456  muladd11r  8472  add32r  8476  cnegexlem2  8492  cnegex  8494  pncan2  8523  addsubass  8526  subadd23  8528  addsub12  8529  subid  8535  subid1  8536  npncan  8537  nppcan3  8540  subsub  8546  nppcan2  8547  nnncan2  8553  npncan3  8554  pnpcan  8555  negdi  8573  mvlraddd  8680  mvlladdd  8681  pnpncand  8691  subdi  8702  mulsub  8718  mulsub2  8719  eqord1  8801  recexap  8971  div32ap  9012  divsubdirap  9028  divmuldivap  9032  divdivdivap  9033  divmuleqap  9037  divcanap6  9039  dmdcanap  9042  divsubdivap  9048  div2negap  9055  div2subap  9157  mvllmulapd  9162  prodgt0gt0  9171  cju  9281  zneo  9726  infrenegsupex  9973  qreccl  10021  mul2lt0rlt0  10139  xnpcan  10253  fzosn  10601  modqid  10764  modqm1p1mod0  10790  modqltm1p1mod  10791  modqmul1  10792  modaddmodup  10802  modaddmodlo  10803  modqsubdir  10808  iseqf1olemkle  10912  iseqf1olemklt  10913  seq3f1olemstep  10929  seq3f1oleml  10931  seqf1oglem2  10935  seqfeq3  10944  seq3distr  10947  expineg2  10963  expm1t  10982  expadd  10996  expaddzaplem  10997  expmulzap  11000  sqsubswap  11014  subsq2  11062  binom2sub  11068  binom3  11072  resq01  11073  facndiv  11155  bcval5  11179  bcn2p1  11187  bcnm1  11189  hashpwfi  11247  hashfibclem  11260  pfxccatpfx2  11487  2shfti  11574  shftcan2  11578  reim0  11604  imval2  11637  cjreim2  11648  cjdivap  11653  cnrecnv  11654  rennim  11746  resqrexlemnm  11762  remsqsqrt  11776  sqrtdiv  11786  sqrtmsq  11789  sqabsadd  11799  sqabssub  11800  absreim  11812  absdivap  11814  absnid  11817  sqabs  11826  abslt  11832  absle  11833  recvalap  11841  abssub  11845  maxabslemlub  11951  infxrnegsupex  12007  mulcn2  12056  reccn2ap  12057  cjcn2  12060  summodclem3  12125  summodclem2a  12126  summodc  12128  zsumdc  12129  fsum3  12132  fisumss  12137  fsumcl2lem  12143  fsumm1  12161  fsum1p  12163  isummulc2  12171  telfsumo  12211  binomlem  12228  bcxmas  12234  arisum  12243  trireciplem  12245  trirecip  12246  geolim2  12257  georeclim  12258  cvgratnnlemfm  12274  cvgratz  12277  mertenslemi1  12280  clim2divap  12285  prodmodclem3  12320  prodmodclem2a  12321  zproddc  12324  fprodseq  12328  fprodssdc  12335  fprod1p  12344  efcan  12421  efexp  12427  efzval  12428  efgt0  12429  eftlub  12435  efltim  12443  resinval  12460  recosval  12461  cosmul  12490  cos2t  12495  cos2tsin  12496  cos01bnd  12503  cos12dec  12513  eirraplem  12522  muldvds1  12561  dvdsexp  12606  oexpneg  12622  divalglemqt  12664  divalglemeunn  12666  divalglemeuneg  12668  divalgmod  12672  flodddiv4t2lthalf  12684  bitsmod  12701  bitsinv1lem  12706  gcdid0  12735  gcdaddm  12739  dvdsgcdidd  12749  rpmulgcd  12781  sqgcd  12784  algcvg  12804  eucalgcvga  12814  eucalg  12815  dvdslcm  12825  lcmeq0  12827  lcmgcd  12834  qredeu  12853  sqnprm  12892  divgcdodd  12899  sqrt2irrlem  12917  sqpweven  12931  2sqpwodd  12932  divnumden  12952  hashdvds  12977  phimullem  12981  eulerthlemrprm  12985  eulerthlemth  12988  odzdvds  13002  pythagtriplem3  13024  pythagtriplem4  13025  pythagtriplem14  13034  pythagtriplem19  13039  pcpremul  13050  pceulem  13051  pcqdiv  13064  pcaddlem  13096  fldivp1  13105  1arithlem4  13123  4sqlem10  13144  mul4sqlem  13150  4sqlem11  13158  4sqlem15  13162  4sqlem16  13163  4sqlem17  13164  ballotfilemfc0  13210  ballotfilemfcc  13211  ballotfilemic  13228  ballotfilem1c  13229  ballotfilemfrceq  13250  ballotfilemrinv0  13254  ennnfonelemhf1o  13282  strslssd  13377  ressbas2d  13399  ressinbasd  13405  topnidg  13583  lidrideqd  13678  grpidd  13680  grprida  13684  gzsumress  13689  ismndd  13727  grpidd2  13823  grpinvid1  13834  grpinvid2  13835  grppnpcan2  13876  grpnpncan  13877  dfgrp3mlem  13880  grpsubpropd2  13887  mhmid  13895  mhmmnd  13896  mulgsubcl  13916  mulgneg  13920  mulgaddcomlem  13925  mulginvinv  13928  mulgdirlem  13933  mulgdir  13934  mulgass  13939  mulgmodid  13941  grpissubg  13974  eqgcpbl  14008  ghmid  14029  ghmmulg  14036  resghm  14040  invghm  14110  gsum0cmn  14131  mgptopng  14203  srgisid  14264  ringidss  14307  ringcom  14309  opprsubgg  14363  unitgrp  14396  1rinv  14408  0unit  14409  rhmdvdsr  14455  lringuplu  14476  subrngpropd  14497  subrgpropd  14534  lmod0vs  14630  lmodvsmmulgdi  14632  lmodvneg1  14639  lmodcom  14642  lmodsubvs  14652  lmodsubdir  14654  lmodpropd  14658  lspsnsub  14730  lspsneq0b  14736  lsppropd  14741  rlmscabas  14769  lidlbas  14787  zringmulg  14905  restopnb  15205  txcnmpt  15297  cnmpt1t  15309  blhalf  15432  xmspropd  15501  mspropd  15502  mpomulcn  15590  ivthreinc  15669  limcimolemlt  15688  dvfre  15734  dveflem  15750  dvef  15751  ply1termlem  15766  plymullem1  15772  sin2kpi  15835  cos2kpi  15836  sin2pim  15837  cos2pim  15838  ptolemy  15848  sincosq2sgn  15851  sincosq3sgn  15852  sincosq4sgn  15853  sinq12gt0  15854  tangtx  15862  sincosq1eq  15863  abssinper  15870  sinkpi  15871  relogeftb  15889  relogoprlem  15892  relogexp  15896  pellexlem1  16005  mpodvdsmulf1o  16018  mersenne  16025  perfectlem1  16027  perfectlem2  16028  perfect  16029  lgsval2lem  16043  lgsdir2lem4  16064  lgsdirprm  16067  lgsdilem2  16069  gausslemma2dlem7  16101  lgseisenlem4  16106  lgsquadlem1  16110  lgsquadlem2  16111  lgsquad2lem1  16114  lgsquad2lem2  16115  2sqlem4  16151  2sqlem6  16153  2sqlem8  16156  clwwlknonel  16587  eupth2fi  16634  dichmul0orlem2  16668  dichmul0orlem3  16669  dichmul0orlem4  16670  peano3nninf  16955  nninfsel  16965  nninffeq  16968  isomninnlem  16984  cvgcmp2nlemabs  16986  trilpolemlt1  16995  trirec0xor  16999  qdiff  17003  ismkvnnlem  17007