Theorem eqtr3d 2200

Description: An equality transitivity equality deduction. (Contributed by NM, 18-Jul-1995.)

Hypotheses

Ref	Expression
eqtr3d.1	⊢ (𝜑 → 𝐴 = 𝐵)
eqtr3d.2	⊢ (𝜑 → 𝐴 = 𝐶)

Assertion

Ref	Expression
eqtr3d	⊢ (𝜑 → 𝐵 = 𝐶)

Proof of Theorem eqtr3d

Step	Hyp	Ref	Expression
1		eqtr3d.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
2	1	eqcomd 2171	. 2 ⊢ (𝜑 → 𝐵 = 𝐴)
3		eqtr3d.2	. 2 ⊢ (𝜑 → 𝐴 = 𝐶)
4	2, 3	eqtrd 2198	1 ⊢ (𝜑 → 𝐵 = 𝐶)

Syntax hints:   → wi 4   = wceq 1343

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 1435  ax-gen 1437  ax-4 1498  ax-17 1514  ax-ext 2147

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

This theorem is referenced by:  3eqtr3d  2206  3eqtr3rd  2207  3eqtr3a  2222  opth  4214  eusvnf  4430  f00  5378  f1imacnv  5448  foimacnv  5449  f1ococnv1  5460  funfvdm  5548  fvmptdf  5572  fndmdif  5589  acexmidlemph  5834  acexmidlemab  5835  ovmpodf  5969  oprssov  5979  grpridd  6034  tfrlemisucaccv  6289  tfr1onlemsucaccv  6305  tfrcllemsucaccv  6318  oav2  6427  omv2  6429  fnsnsplitdc  6469  ecopovtrn  6594  ecopovtrng  6597  map0b  6649  en1  6761  ssenen  6813  fidifsnen  6832  dif1en  6841  undifdc  6885  fidcenumlemr  6916  ordiso2  6996  nnnninfeq2  7089  nninfisollemne  7091  finomni  7100  exmidomni  7102  fodjum  7106  exmidaclem  7160  distrnqg  7324  1qec  7325  prarloclemarch2  7356  nnnq0lem1  7383  nqpnq0nq  7390  distrnq0  7396  prarloclemlt  7430  prmuloclemcalc  7502  ltaprg  7556  prplnqu  7557  recexprlem1ssl  7570  recexprlem1ssu  7571  ltmprr  7579  cauappcvgprlemopl  7583  caucvgprlemopl  7606  caucvgprprlemopl  7634  caucvgprprlemexb  7644  prsrlem1  7679  ltsosr  7701  mulgt0sr  7715  recidpipr  7793  recriota  7827  nntopi  7831  axcaucvglemres  7836  addid2  8033  readdcan  8034  muladd11r  8050  add32r  8054  cnegexlem2  8070  cnegex  8072  pncan2  8101  addsubass  8104  subadd23  8106  addsub12  8107  subid  8113  subid1  8114  npncan  8115  nppcan3  8118  subsub  8124  nppcan2  8125  nnncan2  8131  npncan3  8132  pnpcan  8133  negdi  8151  mvlraddd  8258  mvlladdd  8259  pnpncand  8269  subdi  8279  mulsub  8295  mulsub2  8296  eqord1  8377  recexap  8546  div32ap  8584  divsubdirap  8600  divmuldivap  8604  divdivdivap  8605  divmuleqap  8609  divcanap6  8611  dmdcanap  8614  divsubdivap  8620  div2negap  8627  div2subap  8729  mvllmulapd  8734  prodgt0gt0  8742  cju  8852  zneo  9288  infrenegsupex  9528  qreccl  9576  mul2lt0rlt0  9691  xnpcan  9804  fzosn  10136  modqid  10280  modqm1p1mod0  10306  modqltm1p1mod  10307  modqmul1  10308  modaddmodup  10318  modaddmodlo  10319  modqsubdir  10324  iseqf1olemkle  10415  iseqf1olemklt  10416  seq3f1olemstep  10432  seq3f1oleml  10434  seqfeq3  10443  seq3distr  10444  expineg2  10460  expm1t  10479  expadd  10493  expaddzaplem  10494  expmulzap  10497  sqsubswap  10511  subsq2  10558  binom2sub  10564  binom3  10568  facndiv  10648  bcval5  10672  bcn2p1  10679  bcnm1  10681  2shfti  10769  shftcan2  10773  reim0  10799  imval2  10832  cjreim2  10842  cjdivap  10847  cnrecnv  10848  rennim  10940  resqrexlemnm  10956  remsqsqrt  10970  sqrtdiv  10980  sqrtmsq  10983  sqabsadd  10993  sqabssub  10994  absreim  11006  absdivap  11008  absnid  11011  sqabs  11020  abslt  11026  absle  11027  recvalap  11035  abssub  11039  maxabslemlub  11145  infxrnegsupex  11200  mulcn2  11249  reccn2ap  11250  cjcn2  11253  summodclem3  11317  summodclem2a  11318  summodc  11320  zsumdc  11321  fsum3  11324  fisumss  11329  fsumcl2lem  11335  fsumm1  11353  fsum1p  11355  isummulc2  11363  telfsumo  11403  binomlem  11420  bcxmas  11426  arisum  11435  trireciplem  11437  trirecip  11438  geolim2  11449  georeclim  11450  cvgratnnlemfm  11466  cvgratz  11469  mertenslemi1  11472  clim2divap  11477  prodmodclem3  11512  prodmodclem2a  11513  zproddc  11516  fprodseq  11520  fprodssdc  11527  fprod1p  11536  efcan  11613  efexp  11619  efzval  11620  efgt0  11621  eftlub  11627  efltim  11635  resinval  11652  recosval  11653  cosmul  11682  cos2t  11687  cos2tsin  11688  cos01bnd  11695  cos12dec  11704  eirraplem  11713  muldvds1  11752  dvdsexp  11795  oexpneg  11810  divalglemqt  11852  divalglemeunn  11854  divalglemeuneg  11856  divalgmod  11860  flodddiv4t2lthalf  11870  gcdid0  11909  gcdaddm  11913  dvdsgcdidd  11923  rpmulgcd  11955  sqgcd  11958  algcvg  11976  eucalgcvga  11986  eucalg  11987  dvdslcm  11997  lcmeq0  11999  lcmgcd  12006  qredeu  12025  sqnprm  12064  divgcdodd  12071  sqrt2irrlem  12089  sqpweven  12103  2sqpwodd  12104  divnumden  12124  hashdvds  12149  phimullem  12153  eulerthlemrprm  12157  eulerthlemth  12160  odzdvds  12173  pythagtriplem3  12195  pythagtriplem4  12196  pythagtriplem14  12205  pythagtriplem19  12210  pcpremul  12221  pceulem  12222  pcqdiv  12235  pcaddlem  12266  fldivp1  12274  1arithlem4  12292  4sqlem10  12313  mul4sqlem  12319  ennnfonelemhf1o  12342  strslssd  12436  topnidg  12564  restopnb  12781  txcnmpt  12873  cnmpt1t  12885  blhalf  13008  xmspropd  13077  mspropd  13078  limcimolemlt  13233  dvfre  13274  dveflem  13287  dvef  13288  sin2kpi  13332  cos2kpi  13333  sin2pim  13334  cos2pim  13335  ptolemy  13345  sincosq2sgn  13348  sincosq3sgn  13349  sincosq4sgn  13350  sinq12gt0  13351  tangtx  13359  sincosq1eq  13360  abssinper  13367  sinkpi  13368  relogeftb  13386  relogoprlem  13389  relogexp  13393  lgsval2lem  13511  lgsdir2lem4  13532  lgsdirprm  13535  lgsdilem2  13537  2sqlem4  13554  2sqlem6  13556  2sqlem8  13559  peano3nninf  13847  nninfsel  13857  nninffeq  13860  isomninnlem  13869  cvgcmp2nlemabs  13871  trilpolemlt1  13880  trirec0xor  13884  ismkvnnlem  13891