Theorem eqtr4di 2217

Description: An equality transitivity deduction. (Contributed by NM, 5-Aug-1993.)

Hypotheses

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

Assertion

Ref	Expression
eqtr4di	⊢ (𝜑 → 𝐴 = 𝐶)

Proof of Theorem eqtr4di

Step	Hyp	Ref	Expression
1		eqtr4di.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		eqtr4di.2	. . 3 ⊢ 𝐶 = 𝐵
3	2	eqcomi 2169	. 2 ⊢ 𝐵 = 𝐶
4	1, 3	eqtrdi 2215	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:  3eqtr4g  2224  rabxmdc  3440  relop  4754  csbcnvg  4788  dfiun3g  4861  dfiin3g  4862  resima2  4918  relcnvfld  5137  uniabio  5163  fntpg  5244  dffn5im  5532  dfimafn2  5536  fncnvima2  5606  fmptcof  5652  fcoconst  5656  fnasrng  5665  ffnov  5946  fnovim  5950  fnrnov  5987  foov  5988  funimassov  5991  ovelimab  5992  ofc12  6070  caofinvl  6072  dftpos3  6230  tfr0dm  6290  rdgisucinc  6353  oasuc  6432  ecinxp  6576  phplem1  6818  exmidpw  6874  exmidpweq  6875  unfiin  6891  fidcenumlemr  6920  0ct  7072  ctmlemr  7073  exmidaclem  7164  indpi  7283  nqnq0pi  7379  nq0m0r  7397  addnqpr1  7503  recexgt0sr  7714  suplocsrlempr  7748  recidpipr  7797  recidpirq  7799  axrnegex  7820  nntopi  7835  cnref1o  9588  fztp  10013  fseq1m1p1  10030  fz0to4untppr  10059  frecuzrdgrrn  10343  frecuzrdgsuc  10349  frecuzrdgsuctlem  10358  seq3val  10393  seqvalcd  10394  fser0const  10451  mulexpzap  10495  expaddzap  10499  bcp1m1  10678  cjexp  10835  rexuz3  10932  bdtri  11181  climconst  11231  sumfct  11315  zsumdc  11325  fsum3  11328  sum0  11329  fsumcnv  11378  mertenslem2  11477  zproddc  11520  fprodseq  11524  prod0  11526  prod1dc  11527  prodfct  11528  fprodcnv  11566  ef0lem  11601  efzval  11624  efival  11673  sinbnd  11693  cosbnd  11694  eucalgval  11986  eucalginv  11988  eucalglt  11989  eucalgcvga  11990  eucalg  11991  sqpweven  12107  2sqpwodd  12108  dfphi2  12152  phimullem  12157  prmdiv  12167  odzval  12173  pcval  12228  pczpre  12229  pcrec  12240  ennnfonelemhdmp1  12342  ennnfonelemkh  12345  ressid2  12454  ressval2  12455  topnvalg  12568  ismgm  12588  plusffvalg  12593  grpidvalg  12604  issgrp  12621  istps  12680  cldval  12749  ntrfval  12750  clsfval  12751  neifval  12790  restbasg  12818  tgrest  12819  txval  12905  upxp  12922  uptx  12924  txrest  12926  lmcn2  12930  cnmpt2t  12943  cnmpt2res  12947  imasnopn  12949  psmetxrge0  12982  xmetge0  13015  isxms  13101  isms  13103  bdxmet  13151  qtopbasss  13171  cnblcld  13185  negfcncf  13239  dvfvalap  13300  eldvap  13301  dvidlemap  13310  dvexp2  13326  dvrecap  13327  dveflem  13337  sin0pilem1  13352  ptolemy  13395  coskpi  13419  logbrec  13528  lgslem1  13551  lgsval  13555  lgsval4  13571  lgsfcl3  13572  lgsdilem  13578  lgsdir2lem4  13582  lgsdir2lem5  13583  nninfsellemqall  13905