Theorem eqtr3d 2212

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

Syntax hints:   -> wi 4   = wceq 1353

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 1447  ax-gen 1449  ax-4 1510  ax-17 1526  ax-ext 2159

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

This theorem is referenced by:  3eqtr3d  2218  3eqtr3rd  2219  3eqtr3a  2234  opth  4239  eusvnf  4455  f00  5409  f1imacnv  5480  foimacnv  5481  f1ococnv1  5492  funfvdm  5582  fvmptdf  5606  fndmdif  5624  acexmidlemph  5871  acexmidlemab  5872  ovmpodf  6009  oprssov  6019  tfrlemisucaccv  6329  tfr1onlemsucaccv  6345  tfrcllemsucaccv  6358  oav2  6467  omv2  6469  fnsnsplitdc  6509  ecopovtrn  6635  ecopovtrng  6638  map0b  6690  en1  6802  ssenen  6854  fidifsnen  6873  dif1en  6882  undifdc  6926  fidcenumlemr  6957  ordiso2  7037  nnnninfeq2  7130  nninfisollemne  7132  finomni  7141  exmidomni  7143  fodjum  7147  exmidaclem  7210  distrnqg  7389  1qec  7390  prarloclemarch2  7421  nnnq0lem1  7448  nqpnq0nq  7455  distrnq0  7461  prarloclemlt  7495  prmuloclemcalc  7567  ltaprg  7621  prplnqu  7622  recexprlem1ssl  7635  recexprlem1ssu  7636  ltmprr  7644  cauappcvgprlemopl  7648  caucvgprlemopl  7671  caucvgprprlemopl  7699  caucvgprprlemexb  7709  prsrlem1  7744  ltsosr  7766  mulgt0sr  7780  recidpipr  7858  recriota  7892  nntopi  7896  axcaucvglemres  7901  addlid  8099  readdcan  8100  muladd11r  8116  add32r  8120  cnegexlem2  8136  cnegex  8138  pncan2  8167  addsubass  8170  subadd23  8172  addsub12  8173  subid  8179  subid1  8180  npncan  8181  nppcan3  8184  subsub  8190  nppcan2  8191  nnncan2  8197  npncan3  8198  pnpcan  8199  negdi  8217  mvlraddd  8324  mvlladdd  8325  pnpncand  8335  subdi  8345  mulsub  8361  mulsub2  8362  eqord1  8443  recexap  8613  div32ap  8652  divsubdirap  8668  divmuldivap  8672  divdivdivap  8673  divmuleqap  8677  divcanap6  8679  dmdcanap  8682  divsubdivap  8688  div2negap  8695  div2subap  8797  mvllmulapd  8802  prodgt0gt0  8811  cju  8921  zneo  9357  infrenegsupex  9597  qreccl  9645  mul2lt0rlt0  9762  xnpcan  9875  fzosn  10208  modqid  10352  modqm1p1mod0  10378  modqltm1p1mod  10379  modqmul1  10380  modaddmodup  10390  modaddmodlo  10391  modqsubdir  10396  iseqf1olemkle  10487  iseqf1olemklt  10488  seq3f1olemstep  10504  seq3f1oleml  10506  seqfeq3  10515  seq3distr  10516  expineg2  10532  expm1t  10551  expadd  10565  expaddzaplem  10566  expmulzap  10569  sqsubswap  10583  subsq2  10631  binom2sub  10637  binom3  10641  facndiv  10722  bcval5  10746  bcn2p1  10753  bcnm1  10755  2shfti  10843  shftcan2  10847  reim0  10873  imval2  10906  cjreim2  10916  cjdivap  10921  cnrecnv  10922  rennim  11014  resqrexlemnm  11030  remsqsqrt  11044  sqrtdiv  11054  sqrtmsq  11057  sqabsadd  11067  sqabssub  11068  absreim  11080  absdivap  11082  absnid  11085  sqabs  11094  abslt  11100  absle  11101  recvalap  11109  abssub  11113  maxabslemlub  11219  infxrnegsupex  11274  mulcn2  11323  reccn2ap  11324  cjcn2  11327  summodclem3  11391  summodclem2a  11392  summodc  11394  zsumdc  11395  fsum3  11398  fisumss  11403  fsumcl2lem  11409  fsumm1  11427  fsum1p  11429  isummulc2  11437  telfsumo  11477  binomlem  11494  bcxmas  11500  arisum  11509  trireciplem  11511  trirecip  11512  geolim2  11523  georeclim  11524  cvgratnnlemfm  11540  cvgratz  11543  mertenslemi1  11546  clim2divap  11551  prodmodclem3  11586  prodmodclem2a  11587  zproddc  11590  fprodseq  11594  fprodssdc  11601  fprod1p  11610  efcan  11687  efexp  11693  efzval  11694  efgt0  11695  eftlub  11701  efltim  11709  resinval  11726  recosval  11727  cosmul  11756  cos2t  11761  cos2tsin  11762  cos01bnd  11769  cos12dec  11778  eirraplem  11787  muldvds1  11826  dvdsexp  11870  oexpneg  11885  divalglemqt  11927  divalglemeunn  11929  divalglemeuneg  11931  divalgmod  11935  flodddiv4t2lthalf  11945  gcdid0  11984  gcdaddm  11988  dvdsgcdidd  11998  rpmulgcd  12030  sqgcd  12033  algcvg  12051  eucalgcvga  12061  eucalg  12062  dvdslcm  12072  lcmeq0  12074  lcmgcd  12081  qredeu  12100  sqnprm  12139  divgcdodd  12146  sqrt2irrlem  12164  sqpweven  12178  2sqpwodd  12179  divnumden  12199  hashdvds  12224  phimullem  12228  eulerthlemrprm  12232  eulerthlemth  12235  odzdvds  12248  pythagtriplem3  12270  pythagtriplem4  12271  pythagtriplem14  12280  pythagtriplem19  12285  pcpremul  12296  pceulem  12297  pcqdiv  12310  pcaddlem  12341  fldivp1  12349  1arithlem4  12367  4sqlem10  12388  mul4sqlem  12394  ennnfonelemhf1o  12417  strslssd  12512  ressbas2d  12531  ressinbasd  12536  topnidg  12707  lidrideqd  12807  grpidd  12809  grpridd  12813  ismndd  12846  grpidd2  12922  grpinvid1  12933  grpinvid2  12934  grppnpcan2  12975  grpnpncan  12976  dfgrp3mlem  12979  grpsubpropd2  12986  mhmid  12992  mhmmnd  12993  mulgsubcl  13011  mulgneg  13015  mulgaddcomlem  13020  mulginvinv  13023  mulgdirlem  13028  mulgdir  13029  mulgass  13034  mulgmodid  13036  grpissubg  13068  eqgcpbl  13102  mgptopng  13155  srgisid  13207  ringidss  13250  ringcom  13252  unitgrp  13323  1rinv  13335  0unit  13336  lringuplu  13375  subrgpropd  13407  lmod0vs  13449  lmodvsmmulgdi  13451  lmodvneg1  13458  lmodcom  13461  lmodsubvs  13471  lmodsubdir  13473  lmodpropd  13477  lspsnsub  13546  lspsneq0b  13552  lsppropd  13557  lidlbas  13601  zringmulg  13662  restopnb  13869  txcnmpt  13961  cnmpt1t  13973  blhalf  14096  xmspropd  14165  mspropd  14166  limcimolemlt  14321  dvfre  14362  dveflem  14375  dvef  14376  sin2kpi  14420  cos2kpi  14421  sin2pim  14422  cos2pim  14423  ptolemy  14433  sincosq2sgn  14436  sincosq3sgn  14437  sincosq4sgn  14438  sinq12gt0  14439  tangtx  14447  sincosq1eq  14448  abssinper  14455  sinkpi  14456  relogeftb  14474  relogoprlem  14477  relogexp  14481  lgsval2lem  14599  lgsdir2lem4  14620  lgsdirprm  14623  lgsdilem2  14625  2sqlem4  14653  2sqlem6  14655  2sqlem8  14658  peano3nninf  14945  nninfsel  14955  nninffeq  14958  isomninnlem  14967  cvgcmp2nlemabs  14969  trilpolemlt1  14978  trirec0xor  14982  ismkvnnlem  14989