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  7375  nninfninc  7463  nnnninfeq2  7469  nninfisollemne  7471  finomni  7480  exmidomni  7482  fodjum  7486  exmidaclem  7564  distrnqg  7754  1qec  7755  prarloclemarch2  7786  nnnq0lem1  7813  nqpnq0nq  7820  distrnq0  7826  prarloclemlt  7860  prmuloclemcalc  7932  ltaprg  7986  prplnqu  7987  recexprlem1ssl  8000  recexprlem1ssu  8001  ltmprr  8009  cauappcvgprlemopl  8013  caucvgprlemopl  8036  caucvgprprlemopl  8064  caucvgprprlemexb  8074  prsrlem1  8109  ltsosr  8131  mulgt0sr  8145  recidpipr  8223  recriota  8257  nntopi  8261  axcaucvglemres  8266  addlid  8465  readdcan  8466  muladd11r  8482  add32r  8486  cnegexlem2  8502  cnegex  8504  pncan2  8533  addsubass  8536  subadd23  8538  addsub12  8539  subid  8545  subid1  8546  npncan  8547  nppcan3  8550  subsub  8556  nppcan2  8557  nnncan2  8563  npncan3  8564  pnpcan  8565  negdi  8583  mvlraddd  8690  mvlladdd  8691  pnpncand  8701  subdi  8712  mulsub  8728  mulsub2  8729  eqord1  8811  recexap  8981  div32ap  9022  divsubdirap  9038  divmuldivap  9042  divdivdivap  9043  divmuleqap  9047  divcanap6  9049  dmdcanap  9052  divsubdivap  9058  div2negap  9065  div2subap  9167  mvllmulapd  9172  prodgt0gt0  9181  cju  9291  zneo  9747  infrenegsupex  9994  qreccl  10042  mul2lt0rlt0  10160  xnpcan  10274  fzosn  10623  modqid  10786  modqm1p1mod0  10812  modqltm1p1mod  10813  modqmul1  10814  modaddmodup  10824  modaddmodlo  10825  modqsubdir  10830  iseqf1olemkle  10934  iseqf1olemklt  10935  seq3f1olemstep  10951  seq3f1oleml  10953  seqf1oglem2  10957  seqfeq3  10966  seq3distr  10969  expineg2  10985  expm1t  11004  expadd  11018  expaddzaplem  11019  expmulzap  11022  sqsubswap  11036  subsq2  11084  binom2sub  11090  binom3  11094  resq01  11095  facndiv  11177  bcval5  11201  bcn2p1  11209  bcnm1  11211  hashpwfi  11269  hashfibclem  11282  pfxccatpfx2  11509  2shfti  11596  shftcan2  11600  reim0  11626  imval2  11659  cjreim2  11670  cjdivap  11675  cnrecnv  11676  rennim  11768  resqrexlemnm  11784  remsqsqrt  11798  sqrtdiv  11808  sqrtmsq  11811  sqabsadd  11821  sqabssub  11822  absreim  11834  absdivap  11836  absnid  11839  sqabs  11848  abslt  11854  absle  11855  recvalap  11863  abssub  11867  maxabslemlub  11973  infxrnegsupex  12029  mulcn2  12078  reccn2ap  12079  cjcn2  12082  summodclem3  12147  summodclem2a  12148  summodc  12150  zsumdc  12151  fsum3  12154  fisumss  12159  fsumcl2lem  12165  fsumm1  12183  fsum1p  12185  isummulc2  12193  telfsumo  12233  binomlem  12250  bcxmas  12256  arisum  12265  trireciplem  12267  trirecip  12268  geolim2  12279  georeclim  12280  cvgratnnlemfm  12296  cvgratz  12299  mertenslemi1  12302  clim2divap  12307  prodmodclem3  12342  prodmodclem2a  12343  zproddc  12346  fprodseq  12350  fprodssdc  12357  fprod1p  12366  efcan  12443  efexp  12449  efzval  12450  efgt0  12451  eftlub  12457  efltim  12465  resinval  12482  recosval  12483  cosmul  12512  cos2t  12517  cos2tsin  12518  cos01bnd  12525  cos12dec  12535  eirraplem  12544  muldvds1  12583  dvdsexp  12628  oexpneg  12644  divalglemqt  12686  divalglemeunn  12688  divalglemeuneg  12690  divalgmod  12694  flodddiv4t2lthalf  12706  bitsmod  12723  bitsinv1lem  12728  gcdid0  12757  gcdaddm  12761  dvdsgcdidd  12771  rpmulgcd  12803  sqgcd  12806  algcvg  12826  eucalgcvga  12836  eucalg  12837  dvdslcm  12847  lcmeq0  12849  lcmgcd  12856  qredeu  12875  sqnprm  12914  divgcdodd  12921  sqrt2irrlem  12939  sqpweven  12953  2sqpwodd  12954  divnumden  12974  hashdvds  12999  phimullem  13003  eulerthlemrprm  13007  eulerthlemth  13010  odzdvds  13024  pythagtriplem3  13046  pythagtriplem4  13047  pythagtriplem14  13056  pythagtriplem19  13061  pcpremul  13072  pceulem  13073  pcqdiv  13086  pcaddlem  13118  fldivp1  13127  1arithlem4  13145  4sqlem10  13166  mul4sqlem  13172  4sqlem11  13180  4sqlem15  13184  4sqlem16  13185  4sqlem17  13186  ballotfilemfc0  13232  ballotfilemfcc  13233  ballotfilemic  13250  ballotfilem1c  13251  ballotfilemfrceq  13272  ballotfilemrinv0  13276  ennnfonelemhf1o  13304  strslssd  13399  ressbas2d  13422  ressinbasd  13428  topnidg  13606  lidrideqd  13701  grpidd  13703  grprida  13707  gzsumress  13712  ismndd  13750  grpidd2  13846  grpinvid1  13857  grpinvid2  13858  grppnpcan2  13899  grpnpncan  13900  dfgrp3mlem  13903  grpsubpropd2  13910  mhmid  13918  mhmmnd  13919  mulgsubcl  13939  mulgneg  13943  mulgaddcomlem  13948  mulginvinv  13951  mulgdirlem  13956  mulgdir  13957  mulgass  13962  mulgmodid  13964  grpissubg  13997  eqgcpbl  14031  ghmid  14052  ghmmulg  14059  resghm  14063  invghm  14133  gsum0cmn  14154  mgptopng  14228  srgisid  14290  ringidss  14334  ringcom  14336  opprsubgg  14390  unitgrp  14423  1rinv  14435  0unit  14436  rhmdvdsr  14482  lringuplu  14503  subrngpropd  14524  subrgpropd  14561  lmod0vs  14658  lmodvsmmulgdi  14660  lmodvneg1  14667  lmodcom  14670  lmodsubvs  14680  lmodsubdir  14682  lmodpropd  14686  lspsnsub  14758  lspsneq0b  14764  lsppropd  14769  rlmscabas  14797  lidlbas  14815  zringmulg  14933  restopnb  15282  txcnmpt  15374  cnmpt1t  15386  blhalf  15509  xmspropd  15578  mspropd  15579  mpomulcn  15667  ivthreinc  15746  limcimolemlt  15765  dvfre  15811  dveflem  15827  dvef  15828  ply1termlem  15843  plymullem1  15849  sin2kpi  15912  cos2kpi  15913  sin2pim  15914  cos2pim  15915  ptolemy  15925  sincosq2sgn  15928  sincosq3sgn  15929  sincosq4sgn  15930  sinq12gt0  15931  tangtx  15939  sincosq1eq  15940  abssinper  15947  sinkpi  15948  relogeftb  15966  relogoprlem  15969  relogexp  15973  log2tlbndlog2  16082  birthdaylem2  16088  birthdaylem3  16089  pellexlem1  16091  mpodvdsmulf1o  16104  mersenne  16111  perfectlem1  16113  perfectlem2  16114  perfect  16115  lgsval2lem  16129  lgsdir2lem4  16150  lgsdirprm  16153  lgsdilem2  16155  gausslemma2dlem7  16187  lgseisenlem4  16192  lgsquadlem1  16196  lgsquadlem2  16197  lgsquad2lem1  16200  lgsquad2lem2  16201  2sqlem4  16237  2sqlem6  16239  2sqlem8  16242  clwwlknonel  16673  eupth2fi  16720  dichmul0orlem2  16754  dichmul0orlem3  16755  dichmul0orlem4  16756  peano3nninf  17050  nninfsel  17060  nninffeq  17063  isomninnlem  17079  cvgcmp2nlemabs  17081  trilpolemlt1  17090  trirec0xor  17094  qdiff  17098  ismkvnnlem  17102