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  8466  readdcan  8467  muladd11r  8483  add32r  8487  cnegexlem2  8503  cnegex  8505  pncan2  8534  addsubass  8537  subadd23  8539  addsub12  8540  subid  8546  subid1  8547  npncan  8548  nppcan3  8551  subsub  8557  nppcan2  8558  nnncan2  8564  npncan3  8565  pnpcan  8566  negdi  8584  mvlraddd  8691  mvlladdd  8692  pnpncand  8702  subdi  8713  mulsub  8729  mulsub2  8730  eqord1  8812  recexap  8983  div32ap  9024  divsubdirap  9040  divmuldivap  9044  divdivdivap  9045  divmuleqap  9049  divcanap6  9051  dmdcanap  9054  divsubdivap  9060  div2negap  9067  div2subap  9169  mvllmulapd  9174  prodgt0gt0  9183  cju  9293  zneo  9751  infrenegsupex  10003  qreccl  10051  mul2lt0rlt0  10170  xnpcan  10284  fzosn  10633  modqid  10799  modqm1p1mod0  10825  modqltm1p1mod  10826  modqmul1  10827  modaddmodup  10837  modaddmodlo  10838  modqsubdir  10843  iseqf1olemkle  10947  iseqf1olemklt  10948  seq3f1olemstep  10964  seq3f1oleml  10966  seqf1oglem2  10970  seqfeq3  10979  seq3distr  10982  expineg2  10998  expm1t  11017  expadd  11031  expaddzaplem  11032  expmulzap  11035  sqsubswap  11049  subsq2  11097  binom2sub  11103  binom3  11107  resq01  11108  facndiv  11191  bcval5  11215  bcn2p1  11223  bcnm1  11225  hashpwfi  11283  hashfibclem  11296  pfxccatpfx2  11523  2shfti  11610  shftcan2  11614  reim0  11640  imval2  11673  cjreim2  11684  cjdivap  11689  cnrecnv  11690  rennim  11782  resqrexlemnm  11798  remsqsqrt  11812  sqrtdiv  11822  sqrtmsq  11825  sqabsadd  11835  sqabssub  11836  absreim  11848  absdivap  11850  absnid  11853  sqabs  11863  abslt  11869  absle  11870  recvalap  11878  abssub  11882  maxabslemlub  11988  infxrnegsupex  12045  mulcn2  12094  reccn2ap  12095  cjcn2  12098  summodclem3  12163  summodclem2a  12164  summodc  12166  zsumdc  12167  fsum3  12170  fisumss  12175  fsumcl2lem  12181  fsumm1  12199  fsum1p  12201  isummulc2  12209  telfsumo  12249  binomlem  12266  bcxmas  12272  arisum  12281  trireciplem  12283  trirecip  12284  geolim2  12295  georeclim  12296  cvgratnnlemfm  12312  cvgratz  12315  mertenslemi1  12318  clim2divap  12323  prodmodclem3  12358  prodmodclem2a  12359  zproddc  12362  fprodseq  12366  fprodssdc  12373  fprod1p  12382  efcan  12459  efexp  12465  efzval  12466  efgt0  12467  eftlub  12473  efltim  12481  resinval  12498  recosval  12499  cosmul  12528  cos2t  12533  cos2tsin  12534  cos01bnd  12541  cos12dec  12551  eirraplem  12560  muldvds1  12599  dvdsexp  12644  oexpneg  12660  divalglemqt  12702  divalglemeunn  12704  divalglemeuneg  12706  divalgmod  12710  flodddiv4t2lthalf  12722  bitsmod  12739  bitsinv1lem  12744  gcdid0  12773  gcdaddm  12777  dvdsgcdidd  12787  rpmulgcd  12819  sqgcd  12822  algcvg  12842  eucalgcvga  12852  eucalg  12853  dvdslcm  12863  lcmeq0  12865  lcmgcd  12872  qredeu  12891  sqnprm  12931  divgcdodd  12938  sqrt2irrlem  12956  sqpweven  12971  2sqpwodd  12972  divnumden  12992  hashdvds  13019  phimullem  13023  eulerthlemrprm  13027  eulerthlemth  13030  odzdvds  13044  pythagtriplem3  13066  pythagtriplem4  13067  pythagtriplem14  13076  pythagtriplem19  13081  pcpremul  13092  pceulem  13093  pcqdiv  13106  pcaddlem  13138  fldivp1  13147  1arithlem4  13165  4sqlem10  13186  mul4sqlem  13192  4sqlem11  13200  4sqlem15  13204  4sqlem16  13205  4sqlem17  13206  ballotfilemfc0  13281  ballotfilemfcc  13282  ballotfilemic  13299  ballotfilem1c  13300  ballotfilemfrceq  13321  ballotfilemrinv0  13325  ennnfonelemhf1o  13353  strslssd  13448  ressbas2d  13471  ressinbasd  13477  topnidg  13655  lidrideqd  13750  grpidd  13752  grprida  13756  gzsumress  13761  ismndd  13799  grpidd2  13895  grpinvid1  13906  grpinvid2  13907  grppnpcan2  13948  grpnpncan  13949  dfgrp3mlem  13952  grpsubpropd2  13959  mhmid  13967  mhmmnd  13968  mulgsubcl  13988  mulgneg  13992  mulgaddcomlem  13997  mulginvinv  14000  mulgdirlem  14005  mulgdir  14006  mulgass  14011  mulgmodid  14013  grpissubg  14046  eqgcpbl  14080  ghmid  14101  ghmmulg  14108  resghm  14112  invghm  14182  gsum0cmn  14203  mgptopng  14277  srgisid  14339  ringidss  14383  ringcom  14385  opprsubgg  14439  unitgrp  14472  1rinv  14484  0unit  14485  rhmdvdsr  14531  lringuplu  14552  subrngpropd  14573  subrgpropd  14610  lmod0vs  14707  lmodvsmmulgdi  14709  lmodvneg1  14716  lmodcom  14719  lmodsubvs  14729  lmodsubdir  14731  lmodpropd  14735  lspsnsub  14807  lspsneq0b  14813  lsppropd  14818  rlmscabas  14846  lidlbas  14864  zringmulg  14982  restopnb  15331  txcnmpt  15423  cnmpt1t  15435  blhalf  15558  xmspropd  15627  mspropd  15628  mpomulcn  15716  ivthreinc  15795  limcimolemlt  15814  dvfre  15860  dveflem  15876  dvef  15877  ply1termlem  15892  plymullem1  15898  sin2kpi  15962  cos2kpi  15963  sin2pim  15964  cos2pim  15965  ptolemy  15975  sincosq2sgn  15978  sincosq3sgn  15979  sincosq4sgn  15980  sinq12gt0  15981  tangtx  15989  sincosq1eq  15990  abssinper  15997  sinkpi  15998  relogeftb  16016  relogoprlem  16020  relogexp  16024  log2tlbndlog2  16139  birthdaylem2  16145  birthdaylem3  16146  pellexlem1  16148  ppiqp1le  16173  ppiqltx  16183  mpodvdsmulf1o  16185  ppiqub  16194  mersenne  16195  perfectlem1  16197  perfectlem2  16198  perfect  16199  lgsval2lem  16227  lgsdir2lem4  16248  lgsdirprm  16251  lgsdilem2  16253  gausslemma2dlem7  16285  lgseisenlem4  16290  lgsquadlem1  16294  lgsquadlem2  16295  lgsquad2lem1  16298  lgsquad2lem2  16299  2sqlem4  16335  2sqlem6  16337  2sqlem8  16340  clwwlknonel  16771  eupth2fi  16818  dichmul0orlem2  16852  dichmul0orlem3  16853  dichmul0orlem4  16854  peano3nninf  17148  nninfsel  17158  nninffeq  17161  isomninnlem  17177  cvgcmp2nlemabs  17179  trilpolemlt1  17188  trirec0xor  17192  qdiff  17196  ismkvnnlem  17200