Theorem eqtr3d 2199

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

Syntax hints:   -> wi 4   = wceq 1342

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 1434  ax-gen 1436  ax-4 1497  ax-17 1513  ax-ext 2146

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

This theorem is referenced by:  3eqtr3d  2205  3eqtr3rd  2206  3eqtr3a  2221  opth  4209  eusvnf  4425  f00  5373  f1imacnv  5443  foimacnv  5444  f1ococnv1  5455  funfvdm  5543  fvmptdf  5567  fndmdif  5584  acexmidlemph  5829  acexmidlemab  5830  ovmpodf  5964  oprssov  5974  grpridd  6029  tfrlemisucaccv  6284  tfr1onlemsucaccv  6300  tfrcllemsucaccv  6313  oav2  6422  omv2  6424  fnsnsplitdc  6464  ecopovtrn  6589  ecopovtrng  6592  map0b  6644  en1  6756  ssenen  6808  fidifsnen  6827  dif1en  6836  undifdc  6880  fidcenumlemr  6911  ordiso2  6991  nnnninfeq2  7084  nninfisollemne  7086  finomni  7095  exmidomni  7097  fodjum  7101  exmidaclem  7155  distrnqg  7319  1qec  7320  prarloclemarch2  7351  nnnq0lem1  7378  nqpnq0nq  7385  distrnq0  7391  prarloclemlt  7425  prmuloclemcalc  7497  ltaprg  7551  prplnqu  7552  recexprlem1ssl  7565  recexprlem1ssu  7566  ltmprr  7574  cauappcvgprlemopl  7578  caucvgprlemopl  7601  caucvgprprlemopl  7629  caucvgprprlemexb  7639  prsrlem1  7674  ltsosr  7696  mulgt0sr  7710  recidpipr  7788  recriota  7822  nntopi  7826  axcaucvglemres  7831  addid2  8028  readdcan  8029  muladd11r  8045  add32r  8049  cnegexlem2  8065  cnegex  8067  pncan2  8096  addsubass  8099  subadd23  8101  addsub12  8102  subid  8108  subid1  8109  npncan  8110  nppcan3  8113  subsub  8119  nppcan2  8120  nnncan2  8126  npncan3  8127  pnpcan  8128  negdi  8146  mvlraddd  8253  mvlladdd  8254  pnpncand  8264  subdi  8274  mulsub  8290  mulsub2  8291  eqord1  8372  recexap  8541  div32ap  8579  divsubdirap  8595  divmuldivap  8599  divdivdivap  8600  divmuleqap  8604  divcanap6  8606  dmdcanap  8609  divsubdivap  8615  div2negap  8622  div2subap  8724  mvllmulapd  8729  prodgt0gt0  8737  cju  8847  zneo  9283  infrenegsupex  9523  qreccl  9571  mul2lt0rlt0  9686  xnpcan  9799  fzosn  10130  modqid  10274  modqm1p1mod0  10300  modqltm1p1mod  10301  modqmul1  10302  modaddmodup  10312  modaddmodlo  10313  modqsubdir  10318  iseqf1olemkle  10409  iseqf1olemklt  10410  seq3f1olemstep  10426  seq3f1oleml  10428  seqfeq3  10437  seq3distr  10438  expineg2  10454  expm1t  10473  expadd  10487  expaddzaplem  10488  expmulzap  10491  sqsubswap  10505  subsq2  10552  binom2sub  10557  binom3  10561  facndiv  10641  bcval5  10665  bcn2p1  10672  bcnm1  10674  2shfti  10759  shftcan2  10763  reim0  10789  imval2  10822  cjreim2  10832  cjdivap  10837  cnrecnv  10838  rennim  10930  resqrexlemnm  10946  remsqsqrt  10960  sqrtdiv  10970  sqrtmsq  10973  sqabsadd  10983  sqabssub  10984  absreim  10996  absdivap  10998  absnid  11001  sqabs  11010  abslt  11016  absle  11017  recvalap  11025  abssub  11029  maxabslemlub  11135  infxrnegsupex  11190  mulcn2  11239  reccn2ap  11240  cjcn2  11243  summodclem3  11307  summodclem2a  11308  summodc  11310  zsumdc  11311  fsum3  11314  fisumss  11319  fsumcl2lem  11325  fsumm1  11343  fsum1p  11345  isummulc2  11353  telfsumo  11393  binomlem  11410  bcxmas  11416  arisum  11425  trireciplem  11427  trirecip  11428  geolim2  11439  georeclim  11440  cvgratnnlemfm  11456  cvgratz  11459  mertenslemi1  11462  clim2divap  11467  prodmodclem3  11502  prodmodclem2a  11503  zproddc  11506  fprodseq  11510  fprodssdc  11517  fprod1p  11526  efcan  11603  efexp  11609  efzval  11610  efgt0  11611  eftlub  11617  efltim  11625  resinval  11642  recosval  11643  cosmul  11672  cos2t  11677  cos2tsin  11678  cos01bnd  11685  cos12dec  11694  eirraplem  11703  muldvds1  11742  dvdsexp  11784  oexpneg  11799  divalglemqt  11841  divalglemeunn  11843  divalglemeuneg  11845  divalgmod  11849  flodddiv4t2lthalf  11859  gcdid0  11898  gcdaddm  11902  dvdsgcdidd  11912  rpmulgcd  11944  sqgcd  11947  algcvg  11959  eucalgcvga  11969  eucalg  11970  dvdslcm  11980  lcmeq0  11982  lcmgcd  11989  qredeu  12008  sqnprm  12047  divgcdodd  12052  sqrt2irrlem  12070  sqpweven  12084  2sqpwodd  12085  divnumden  12105  hashdvds  12130  phimullem  12134  eulerthlemrprm  12138  eulerthlemth  12141  odzdvds  12154  pythagtriplem3  12176  pythagtriplem4  12177  pythagtriplem14  12186  pythagtriplem19  12191  pcpremul  12202  pceulem  12203  pcqdiv  12216  pcaddlem  12247  fldivp1  12255  ennnfonelemhf1o  12283  strslssd  12377  topnidg  12505  restopnb  12722  txcnmpt  12814  cnmpt1t  12826  blhalf  12949  xmspropd  13018  mspropd  13019  limcimolemlt  13174  dvfre  13215  dveflem  13228  dvef  13229  sin2kpi  13273  cos2kpi  13274  sin2pim  13275  cos2pim  13276  ptolemy  13286  sincosq2sgn  13289  sincosq3sgn  13290  sincosq4sgn  13291  sinq12gt0  13292  tangtx  13300  sincosq1eq  13301  abssinper  13308  sinkpi  13309  relogeftb  13327  relogoprlem  13330  relogexp  13334  peano3nninf  13721  nninfsel  13731  nninffeq  13734  isomninnlem  13743  cvgcmp2nlemabs  13745  trilpolemlt1  13754  trirec0xor  13758  ismkvnnlem  13765