Theorem eqtr4di 2205

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 2158	. 2 ⊢ 𝐵 = 𝐶
4	1, 3	eqtrdi 2203	1 ⊢ (𝜑 → 𝐴 = 𝐶)

Syntax hints:   → wi 4   = wceq 1332

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 1424  ax-gen 1426  ax-4 1487  ax-17 1503  ax-ext 2136

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

This theorem is referenced by:  3eqtr4g  2212  rabxmdc  3421  relop  4729  csbcnvg  4763  dfiun3g  4836  dfiin3g  4837  resima2  4893  relcnvfld  5112  uniabio  5138  fntpg  5219  dffn5im  5507  dfimafn2  5511  fncnvima2  5581  fmptcof  5627  fcoconst  5631  fnasrng  5640  ffnov  5915  fnovim  5919  fnrnov  5956  foov  5957  funimassov  5960  ovelimab  5961  ofc12  6042  caofinvl  6044  dftpos3  6199  tfr0dm  6259  rdgisucinc  6322  oasuc  6400  ecinxp  6544  phplem1  6786  exmidpw  6842  exmidpweq  6843  unfiin  6859  fidcenumlemr  6888  0ct  7037  ctmlemr  7038  exmidaclem  7122  indpi  7241  nqnq0pi  7337  nq0m0r  7355  addnqpr1  7461  recexgt0sr  7672  suplocsrlempr  7706  recidpipr  7755  recidpirq  7757  axrnegex  7778  nntopi  7793  cnref1o  9537  fztp  9958  fseq1m1p1  9975  frecuzrdgrrn  10285  frecuzrdgsuc  10291  frecuzrdgsuctlem  10300  seq3val  10335  seqvalcd  10336  fser0const  10393  mulexpzap  10437  expaddzap  10441  bcp1m1  10616  cjexp  10770  rexuz3  10867  bdtri  11116  climconst  11164  sumfct  11248  zsumdc  11258  fsum3  11261  sum0  11262  fsumcnv  11311  mertenslem2  11410  zproddc  11453  fprodseq  11457  prod0  11459  prod1dc  11460  prodfct  11461  fprodcnv  11499  ef0lem  11534  efzval  11557  efival  11606  sinbnd  11626  cosbnd  11627  eucalgval  11902  eucalginv  11904  eucalglt  11905  eucalgcvga  11906  eucalg  11907  sqpweven  12020  2sqpwodd  12021  dfphi2  12063  phimullem  12068  ennnfonelemhdmp1  12089  ennnfonelemkh  12092  ressid2  12188  ressval2  12189  topnvalg  12302  istps  12369  cldval  12438  ntrfval  12439  clsfval  12440  neifval  12479  restbasg  12507  tgrest  12508  txval  12594  upxp  12611  uptx  12613  txrest  12615  lmcn2  12619  cnmpt2t  12632  cnmpt2res  12636  imasnopn  12638  psmetxrge0  12671  xmetge0  12704  isxms  12790  isms  12792  bdxmet  12840  qtopbasss  12860  cnblcld  12874  negfcncf  12928  dvfvalap  12989  eldvap  12990  dvidlemap  12999  dvexp2  13015  dvrecap  13016  dveflem  13026  sin0pilem1  13041  ptolemy  13084  coskpi  13108  logbrec  13216  nninfsellemqall  13528