Theorem eqtr3d 2172

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

Syntax hints:   -> wi 4   = wceq 1331

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-gen 1425  ax-4 1487  ax-17 1506  ax-ext 2119

This theorem depends on definitions:  df-bi 116  df-cleq 2130

This theorem is referenced by:  3eqtr3d  2178  3eqtr3rd  2179  3eqtr3a  2194  opth  4154  eusvnf  4369  f00  5309  f1imacnv  5377  foimacnv  5378  f1ococnv1  5389  funfvdm  5477  fvmptdf  5501  fndmdif  5518  acexmidlemph  5760  acexmidlemab  5761  ovmpodf  5895  oprssov  5905  grpridd  5960  tfrlemisucaccv  6215  tfr1onlemsucaccv  6231  tfrcllemsucaccv  6244  oav2  6352  omv2  6354  fnsnsplitdc  6394  ecopovtrn  6519  ecopovtrng  6522  map0b  6574  en1  6686  ssenen  6738  fidifsnen  6757  dif1en  6766  undifdc  6805  fidcenumlemr  6836  ordiso2  6913  finomni  7005  exmidomni  7007  fodjum  7011  exmidaclem  7057  distrnqg  7188  1qec  7189  prarloclemarch2  7220  nnnq0lem1  7247  nqpnq0nq  7254  distrnq0  7260  prarloclemlt  7294  prmuloclemcalc  7366  ltaprg  7420  prplnqu  7421  recexprlem1ssl  7434  recexprlem1ssu  7435  ltmprr  7443  cauappcvgprlemopl  7447  caucvgprlemopl  7470  caucvgprprlemopl  7498  caucvgprprlemexb  7508  prsrlem1  7543  ltsosr  7565  mulgt0sr  7579  recidpipr  7657  recriota  7691  nntopi  7695  axcaucvglemres  7700  addid2  7894  readdcan  7895  muladd11r  7911  add32r  7915  cnegexlem2  7931  cnegex  7933  pncan2  7962  addsubass  7965  subadd23  7967  addsub12  7968  subid  7974  subid1  7975  npncan  7976  nppcan3  7979  subsub  7985  nppcan2  7986  nnncan2  7992  npncan3  7993  pnpcan  7994  negdi  8012  mvlraddd  8119  mvlladdd  8120  pnpncand  8130  subdi  8140  mulsub  8156  mulsub2  8157  eqord1  8238  recexap  8407  div32ap  8445  divsubdirap  8461  divmuldivap  8465  divdivdivap  8466  divmuleqap  8470  divcanap6  8472  dmdcanap  8475  divsubdivap  8481  div2negap  8488  div2subap  8589  mvllmulapd  8594  prodgt0gt0  8602  cju  8712  zneo  9145  infrenegsupex  9382  qreccl  9427  mul2lt0rlt0  9539  xnpcan  9648  fzosn  9975  modqid  10115  modqm1p1mod0  10141  modqltm1p1mod  10142  modqmul1  10143  modaddmodup  10153  modaddmodlo  10154  modqsubdir  10159  iseqf1olemkle  10250  iseqf1olemklt  10251  seq3f1olemstep  10267  seq3f1oleml  10269  seqfeq3  10278  seq3distr  10279  expineg2  10295  expm1t  10314  expadd  10328  expaddzaplem  10329  expmulzap  10332  sqsubswap  10346  subsq2  10393  binom2sub  10398  binom3  10402  facndiv  10478  bcval5  10502  bcn2p1  10509  bcnm1  10511  2shfti  10596  shftcan2  10600  reim0  10626  imval2  10659  cjreim2  10669  cjdivap  10674  cnrecnv  10675  rennim  10767  resqrexlemnm  10783  remsqsqrt  10797  sqrtdiv  10807  sqrtmsq  10810  sqabsadd  10820  sqabssub  10821  absreim  10833  absdivap  10835  absnid  10838  sqabs  10847  abslt  10853  absle  10854  recvalap  10862  abssub  10866  maxabslemlub  10972  infxrnegsupex  11025  mulcn2  11074  reccn2ap  11075  cjcn2  11078  summodclem3  11142  summodclem2a  11143  summodc  11145  zsumdc  11146  fsum3  11149  fisumss  11154  fsumcl2lem  11160  fsumm1  11178  fsum1p  11180  isummulc2  11188  telfsumo  11228  binomlem  11245  bcxmas  11251  arisum  11260  trireciplem  11262  trirecip  11263  geolim2  11274  georeclim  11275  cvgratnnlemfm  11291  cvgratz  11294  mertenslemi1  11297  clim2divap  11302  efcan  11371  efexp  11377  efzval  11378  efgt0  11379  eftlub  11385  efltim  11393  resinval  11411  recosval  11412  cosmul  11441  cos2t  11446  cos2tsin  11447  cos01bnd  11454  cos12dec  11463  eirraplem  11472  muldvds1  11507  dvdsexp  11548  oexpneg  11563  divalglemqt  11605  divalglemeunn  11607  divalglemeuneg  11609  divalgmod  11613  flodddiv4t2lthalf  11623  gcdid0  11657  gcdaddm  11661  dvdsgcdidd  11671  rpmulgcd  11703  sqgcd  11706  algcvg  11718  eucalgcvga  11728  eucalg  11729  dvdslcm  11739  lcmeq0  11741  lcmgcd  11748  qredeu  11767  sqnprm  11805  divgcdodd  11810  sqrt2irrlem  11828  sqpweven  11842  2sqpwodd  11843  divnumden  11863  hashdvds  11886  phimullem  11890  ennnfonelemhf1o  11915  strslssd  11994  topnidg  12122  restopnb  12339  txcnmpt  12431  cnmpt1t  12443  blhalf  12566  xmspropd  12635  mspropd  12636  limcimolemlt  12791  dvfre  12832  dveflem  12844  dvef  12845  sin2kpi  12881  cos2kpi  12882  sin2pim  12883  cos2pim  12884  ptolemy  12894  sincosq2sgn  12897  sincosq3sgn  12898  sincosq4sgn  12899  sinq12gt0  12900  tangtx  12908  sincosq1eq  12909  abssinper  12916  sinkpi  12917  peano3nninf  13190  nninfsel  13202  nninffeq  13205  isomninnlem  13214  cvgcmp2nlemabs  13216  trilpolemlt1  13223