Theorem eqtr3d 2115

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 2086	. 2 ⊢ (𝜑 → 𝐵 = 𝐴)
3		eqtr3d.2	. 2 ⊢ (𝜑 → 𝐴 = 𝐶)
4	2, 3	eqtrd 2113	1 ⊢ (𝜑 → 𝐵 = 𝐶)

Syntax hints:   → wi 4   = wceq 1284

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1376  ax-gen 1378  ax-4 1440  ax-17 1459  ax-ext 2063

This theorem depends on definitions:  df-bi 115  df-cleq 2074

This theorem is referenced by:  3eqtr3d  2121  3eqtr3rd  2122  3eqtr3a  2137  opth  3992  eusvnf  4203  f00  5101  f1imacnv  5163  foimacnv  5164  f1ococnv1  5175  funfvdm  5257  fvmptdf  5279  fndmdif  5293  acexmidlemph  5525  acexmidlemab  5526  ovmpt2df  5652  oprssov  5662  grpridd  5717  tfrlemisucaccv  5962  oav2  6066  omv2  6068  ecopovtrn  6226  ecopovtrng  6229  en1  6302  fidifsnen  6355  dif1en  6364  ordiso2  6446  distrnqg  6577  1qec  6578  prarloclemarch2  6609  nnnq0lem1  6636  nqpnq0nq  6643  distrnq0  6649  prarloclemlt  6683  prmuloclemcalc  6755  ltaprg  6809  prplnqu  6810  recexprlem1ssl  6823  recexprlem1ssu  6824  ltmprr  6832  cauappcvgprlemopl  6836  caucvgprlemopl  6859  caucvgprprlemopl  6887  caucvgprprlemexb  6897  prsrlem1  6919  ltsosr  6941  mulgt0sr  6954  recidpipr  7024  recriota  7056  nntopi  7060  axcaucvglemres  7065  addid2  7247  readdcan  7248  muladd11r  7264  add32r  7268  cnegexlem2  7284  cnegex  7286  pncan2  7315  addsubass  7318  subadd23  7320  addsub12  7321  subid  7327  subid1  7328  npncan  7329  nppcan3  7332  subsub  7338  nppcan2  7339  nnncan2  7345  npncan3  7346  pnpcan  7347  negdi  7365  mvlraddd  7471  pnpncand  7479  subdi  7489  mulsub  7505  mulsub2  7506  recexap  7743  div32ap  7780  divsubdirap  7796  divmuldivap  7800  divdivdivap  7801  divmuleqap  7805  divcanap6  7807  dmdcanap  7810  divsubdivap  7816  div2negap  7823  mvllmulapd  7921  prodgt0gt0  7929  cju  8038  zneo  8448  infrenegsupex  8682  qreccl  8727  fzosn  9214  modqid  9351  modqm1p1mod0  9377  modqltm1p1mod  9378  modqmul1  9379  modaddmodup  9389  modaddmodlo  9390  modqsubdir  9395  iseqdistr  9470  expineg2  9485  expm1t  9504  expadd  9518  expaddzaplem  9519  expmulzap  9522  sqsubswap  9536  subsq2  9582  binom2sub  9587  binom3  9590  facndiv  9666  ibcval5  9690  bcn2p1  9697  bcnm1  9699  2shfti  9719  shftcan2  9723  reim0  9748  imval2  9781  cjreim2  9791  cjdivap  9796  cnrecnv  9797  rennim  9888  resqrexlemnm  9904  remsqsqrt  9918  sqrtdiv  9928  sqrtmsq  9931  sqabsadd  9941  sqabssub  9942  absreim  9954  absdivap  9956  absnid  9959  sqabs  9968  abslt  9974  absle  9975  recvalap  9983  abssub  9987  maxabslemlub  10093  mulcn2  10151  cjcn2  10154  muldvds1  10220  dvdsexp  10261  oexpneg  10276  divalglemqt  10319  divalglemeunn  10321  divalglemeuneg  10323  divalgmod  10327  flodddiv4t2lthalf  10337  gcdid0  10371  gcdaddm  10375  rpmulgcd  10415  sqgcd  10418  ialgcvg  10430  eucialgcvga  10440  eucialg  10441  dvdslcm  10451  lcmeq0  10453  lcmgcd  10460  qredeu  10479  sqnprm  10517  divgcdodd  10522  sqrt2irrlem  10540  sqpweven  10553  2sqpwodd  10554