Theorem eqtr4di 2280

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

Syntax hints:   → wi 4   = wceq 1395

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 1493  ax-gen 1495  ax-4 1556  ax-17 1572  ax-ext 2211

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

This theorem is referenced by:  3eqtr4g  2287  rabxmdc  3523  ifpprsnssdc  3774  relop  4872  csbcnvg  4906  dfiun3g  4981  dfiin3g  4982  resima2  5039  relcnvfld  5262  uniabio  5289  fntpg  5377  dffn5im  5681  dfimafn2  5685  fncnvima2  5758  fmptcof  5804  fcoconst  5808  fnasrng  5817  funopsn  5819  fncofn  5821  ffnov  6114  fnovim  6119  fnrnov  6157  foov  6158  funimassov  6161  ovelimab  6162  ofc12  6248  caofinvl  6250  dftpos3  6414  tfr0dm  6474  rdgisucinc  6537  oasuc  6618  ecinxp  6765  phplem1  7021  exmidpw  7081  exmidpweq  7082  unfiin  7099  fidcenumlemr  7133  0ct  7285  ctmlemr  7286  exmidaclem  7401  pw1m  7420  indpi  7540  nqnq0pi  7636  nq0m0r  7654  addnqpr1  7760  recexgt0sr  7971  suplocsrlempr  8005  recidpipr  8054  recidpirq  8056  axrnegex  8077  nntopi  8092  cnref1o  9858  fztp  10286  fseq1m1p1  10303  fz0to4untppr  10332  frecuzrdgrrn  10642  frecuzrdgsuc  10648  frecuzrdgsuctlem  10657  seq3val  10694  seqvalcd  10695  fser0const  10769  mulexpzap  10813  expaddzap  10817  bcp1m1  10999  hash2en  11078  iswrdiz  11091  pfxccatin12lem2c  11277  cjexp  11419  rexuz3  11516  bdtri  11766  climconst  11816  sumfct  11900  zsumdc  11910  fsum3  11913  sum0  11914  fsumcnv  11963  mertenslem2  12062  zproddc  12105  fprodseq  12109  prod0  12111  prod1dc  12112  prodfct  12113  fprodcnv  12151  ef0lem  12186  efzval  12209  efival  12258  sinbnd  12278  cosbnd  12279  eucalgval  12591  eucalginv  12593  eucalglt  12594  eucalgcvga  12595  eucalg  12596  sqpweven  12712  2sqpwodd  12713  dfphi2  12757  phimullem  12762  prmdiv  12772  odzval  12779  pcval  12834  pczpre  12835  pcrec  12846  4sqlem17  12945  ennnfonelemhdmp1  12995  ennnfonelemkh  12998  ressinbasd  13122  restid2  13296  topnvalg  13299  prdsval  13321  prdsbas3  13335  pwsval  13339  pwsbas  13340  pwselbasb  13341  pwsplusgval  13343  pwsmulrval  13344  imasival  13354  imasplusg  13356  qusval  13371  xpsval  13400  ismgm  13405  plusffvalg  13410  grpidvalg  13421  igsumvalx  13437  issgrp  13451  ismnddef  13466  pws0g  13499  ismhm  13509  isgrp  13554  grpn0  13583  grpinvfvalg  13590  grpsubfvalg  13593  pwsinvg  13660  mulgfvalg  13673  mulgval  13674  mulgnn0p1  13685  issubg  13725  isnsg  13754  eqgfval  13774  quseccl0g  13783  isghm  13795  conjsubg  13829  conjsubgen  13830  iscmn  13845  mgpvalg  13901  isrng  13912  issrg  13943  isring  13978  iscrng  13981  opprvalg  14047  dfrhm2  14133  isnzr  14160  islring  14171  issubrg  14200  rrgval  14241  isdomn  14248  islmod  14270  scaffvalg  14285  lsssetm  14335  lspfval  14367  2idlval  14481  2idlvalg  14482  mulgrhm2  14589  zlmval  14606  znval  14615  znzrhfo  14627  znle2  14631  psrval  14645  mplvalcoe  14669  istps  14721  cldval  14788  ntrfval  14789  clsfval  14790  neifval  14829  restbasg  14857  tgrest  14858  txval  14944  upxp  14961  uptx  14963  txrest  14965  lmcn2  14969  cnmpt2t  14982  cnmpt2res  14986  imasnopn  14988  psmetxrge0  15021  xmetge0  15054  isxms  15140  isms  15142  bdxmet  15190  qtopbasss  15210  cnblcld  15224  mpomulcn  15255  negfcncf  15295  dvfvalap  15370  eldvap  15371  dvidlemap  15380  dvidrelem  15381  dvidsslem  15382  dvexp2  15401  dvrecap  15402  dveflem  15415  plyconst  15434  plycolemc  15447  sin0pilem1  15470  ptolemy  15513  coskpi  15537  logbrec  15649  mpodvdsmulf1o  15679  fsumdvdsmul  15680  lgslem1  15694  lgsval  15698  lgsval4  15714  lgsfcl3  15715  lgsdilem  15721  lgsdir2lem4  15725  lgsdir2lem5  15726  gausslemma2dlem5  15760  lgsquadlem2  15772  iedgedgg  15876  isuhgrm  15886  isushgrm  15887  isupgren  15910  isumgren  15920  isuspgren  15970  isusgren  15971  usgrstrrepeen  16044  vtxdgfval  16047  wksfval  16063  ifpsnprss  16084  clwwlkg  16131  nninfsellemqall  16441