Theorem eqtr4di 2255

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

Syntax hints:   → wi 4   = wceq 1372

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1469  ax-gen 1471  ax-4 1532  ax-17 1548  ax-ext 2186

This theorem depends on definitions:  df-bi 117  df-cleq 2197

This theorem is referenced by:  3eqtr4g  2262  rabxmdc  3491  relop  4826  csbcnvg  4860  dfiun3g  4933  dfiin3g  4934  resima2  4990  relcnvfld  5213  uniabio  5239  fntpg  5324  dffn5im  5618  dfimafn2  5622  fncnvima2  5695  fmptcof  5741  fcoconst  5745  fnasrng  5754  ffnov  6039  fnovim  6044  fnrnov  6082  foov  6083  funimassov  6086  ovelimab  6087  ofc12  6172  caofinvl  6174  dftpos3  6338  tfr0dm  6398  rdgisucinc  6461  oasuc  6540  ecinxp  6687  phplem1  6931  exmidpw  6987  exmidpweq  6988  unfiin  7005  fidcenumlemr  7039  0ct  7191  ctmlemr  7192  exmidaclem  7302  indpi  7437  nqnq0pi  7533  nq0m0r  7551  addnqpr1  7657  recexgt0sr  7868  suplocsrlempr  7902  recidpipr  7951  recidpirq  7953  axrnegex  7974  nntopi  7989  cnref1o  9754  fztp  10182  fseq1m1p1  10199  fz0to4untppr  10228  frecuzrdgrrn  10534  frecuzrdgsuc  10540  frecuzrdgsuctlem  10549  seq3val  10586  seqvalcd  10587  fser0const  10661  mulexpzap  10705  expaddzap  10709  bcp1m1  10891  iswrdiz  10976  cjexp  11123  rexuz3  11220  bdtri  11470  climconst  11520  sumfct  11604  zsumdc  11614  fsum3  11617  sum0  11618  fsumcnv  11667  mertenslem2  11766  zproddc  11809  fprodseq  11813  prod0  11815  prod1dc  11816  prodfct  11817  fprodcnv  11855  ef0lem  11890  efzval  11913  efival  11962  sinbnd  11982  cosbnd  11983  eucalgval  12295  eucalginv  12297  eucalglt  12298  eucalgcvga  12299  eucalg  12300  sqpweven  12416  2sqpwodd  12417  dfphi2  12461  phimullem  12466  prmdiv  12476  odzval  12483  pcval  12538  pczpre  12539  pcrec  12550  4sqlem17  12649  ennnfonelemhdmp1  12699  ennnfonelemkh  12702  ressinbasd  12825  restid2  12998  topnvalg  13001  prdsval  13023  prdsbas3  13037  pwsval  13041  pwsbas  13042  pwselbasb  13043  pwsplusgval  13045  pwsmulrval  13046  imasival  13056  imasplusg  13058  qusval  13073  xpsval  13102  ismgm  13107  plusffvalg  13112  grpidvalg  13123  igsumvalx  13139  issgrp  13153  ismnddef  13168  pws0g  13201  ismhm  13211  isgrp  13256  grpn0  13285  grpinvfvalg  13292  grpsubfvalg  13295  pwsinvg  13362  mulgfvalg  13375  mulgval  13376  mulgnn0p1  13387  issubg  13427  isnsg  13456  eqgfval  13476  quseccl0g  13485  isghm  13497  conjsubg  13531  conjsubgen  13532  iscmn  13547  mgpvalg  13603  isrng  13614  issrg  13645  isring  13680  iscrng  13683  opprvalg  13749  dfrhm2  13834  isnzr  13861  islring  13872  issubrg  13901  rrgval  13942  isdomn  13949  islmod  13971  scaffvalg  13986  lsssetm  14036  lspfval  14068  2idlval  14182  2idlvalg  14183  mulgrhm2  14290  zlmval  14307  znval  14316  znzrhfo  14328  znle2  14332  psrval  14346  mplvalcoe  14370  istps  14422  cldval  14489  ntrfval  14490  clsfval  14491  neifval  14530  restbasg  14558  tgrest  14559  txval  14645  upxp  14662  uptx  14664  txrest  14666  lmcn2  14670  cnmpt2t  14683  cnmpt2res  14687  imasnopn  14689  psmetxrge0  14722  xmetge0  14755  isxms  14841  isms  14843  bdxmet  14891  qtopbasss  14911  cnblcld  14925  mpomulcn  14956  negfcncf  14996  dvfvalap  15071  eldvap  15072  dvidlemap  15081  dvidrelem  15082  dvidsslem  15083  dvexp2  15102  dvrecap  15103  dveflem  15116  plyconst  15135  plycolemc  15148  sin0pilem1  15171  ptolemy  15214  coskpi  15238  logbrec  15350  mpodvdsmulf1o  15380  fsumdvdsmul  15381  lgslem1  15395  lgsval  15399  lgsval4  15415  lgsfcl3  15416  lgsdilem  15422  lgsdir2lem4  15426  lgsdir2lem5  15427  gausslemma2dlem5  15461  lgsquadlem2  15473  nninfsellemqall  15816