Theorem eqtr4di 2283

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

Syntax hints:   → wi 4   = wceq 1398

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575  ax-ext 2214

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

This theorem is referenced by:  3eqtr4g  2290  rabxmdc  3540  ifpprsnssdc  3799  relop  4905  csbcnvg  4939  dfiun3g  5014  dfiin3g  5015  resima2  5072  relcnvfld  5296  uniabio  5323  fntpg  5412  dffn5im  5722  dfimafn2  5726  fncnvima2  5799  fmptcof  5844  fcoconst  5848  fnasrng  5858  funopsn  5860  fncofn  5862  ffnov  6157  fnovim  6162  fnrnov  6200  foov  6201  funimassov  6204  ovelimab  6205  ofc12  6290  caofinvl  6292  dftpos3  6493  tfr0dm  6553  rdgisucinc  6616  oasuc  6697  ecinxp  6844  mapunen  7104  phplem1  7106  exmidpw  7168  exmidpweq  7169  unfiin  7186  fidcenumlemr  7225  0ct  7398  ctmlemr  7399  exmidaclem  7515  pw1m  7534  indpi  7657  nqnq0pi  7753  nq0m0r  7771  addnqpr1  7877  recexgt0sr  8088  suplocsrlempr  8122  recidpipr  8171  recidpirq  8173  axrnegex  8194  nntopi  8209  fcdmnn0supp  9548  fcdmnn0suppg  9550  cnref1o  9983  fztp  10412  fseq1m1p1  10429  fz0to4untppr  10458  frecuzrdgrrn  10770  frecuzrdgsuc  10776  frecuzrdgsuctlem  10785  seq3val  10822  seqvalcd  10823  fser0const  10897  mulexpzap  10941  expaddzap  10945  bcp1m1  11127  hashfibclem  11206  hash2en  11215  iswrdiz  11231  pfxccatin12lem2c  11422  cjexp  11578  rexuz3  11675  bdtri  11925  climconst  11975  sumfct  12059  zsumdc  12070  fsum3  12073  sum0  12074  fsumcnv  12123  mertenslem2  12222  zproddc  12265  fprodseq  12269  prod0  12271  prod1dc  12272  prodfct  12273  fprodcnv  12311  ef0lem  12346  efzval  12369  efival  12418  sinbnd  12438  cosbnd  12439  eucalgval  12751  eucalginv  12753  eucalglt  12754  eucalgcvga  12755  eucalg  12756  sqpweven  12872  2sqpwodd  12873  dfphi2  12917  phimullem  12922  prmdiv  12932  odzval  12939  pcval  12994  pczpre  12995  pcrec  13006  4sqlem17  13105  ennnfonelemhdmp1  13160  ennnfonelemkh  13163  ressinbasd  13287  restid2  13461  topnvalg  13464  prdsval  13486  prdsbas3  13500  pwsval  13504  pwsbas  13505  pwselbasb  13506  pwsplusgval  13508  pwsmulrval  13509  imasival  13519  imasplusg  13521  qusval  13536  xpsval  13565  ismgm  13570  plusffvalg  13575  grpidvalg  13586  igsumvalx  13602  issgrp  13616  ismnddef  13631  pws0g  13664  ismhm  13674  isgrp  13719  grpn0  13748  grpinvfvalg  13755  grpsubfvalg  13758  pwsinvg  13825  mulgfvalg  13838  mulgval  13839  mulgnn0p1  13850  issubg  13890  isnsg  13919  eqgfval  13939  quseccl0g  13948  isghm  13960  conjsubg  13994  conjsubgen  13995  iscmn  14010  mgpvalg  14067  isrng  14078  issrg  14109  isring  14144  iscrng  14147  opprvalg  14213  dfrhm2  14299  isnzr  14326  islring  14337  issubrg  14366  rrgval  14407  isdomn  14415  islmod  14439  scaffvalg  14454  lsssetm  14504  lspfval  14536  2idlval  14650  2idlvalg  14651  mulgrhm2  14758  zlmval  14775  znval  14784  znzrhfo  14796  znle2  14800  psrval  14814  mplvalcoe  14845  istps  14897  cldval  14964  ntrfval  14965  clsfval  14966  neifval  15005  restbasg  15033  tgrest  15034  txval  15120  upxp  15137  uptx  15139  txrest  15141  lmcn2  15145  cnmpt2t  15158  cnmpt2res  15162  imasnopn  15164  psmetxrge0  15197  xmetge0  15230  isxms  15316  isms  15318  bdxmet  15366  qtopbasss  15386  cnblcld  15400  mpomulcn  15431  negfcncf  15471  dvfvalap  15546  eldvap  15547  dvidlemap  15556  dvidrelem  15557  dvidsslem  15558  dvexp2  15577  dvrecap  15578  dveflem  15591  plyconst  15610  plycolemc  15623  sin0pilem1  15646  ptolemy  15689  coskpi  15713  logbrec  15825  mpodvdsmulf1o  15858  fsumdvdsmul  15859  lgslem1  15873  lgsval  15877  lgsval4  15893  lgsfcl3  15894  lgsdilem  15900  lgsdir2lem4  15904  lgsdir2lem5  15905  gausslemma2dlem5  15939  lgsquadlem2  15951  iedgedgg  16056  isuhgrm  16066  isushgrm  16067  isupgren  16090  isumgren  16100  isuspgren  16152  isusgren  16153  usgrstrrepeen  16226  vtxdgfval  16283  wksfval  16317  ifpsnprss  16338  clwwlkg  16388  clwwlkn1  16413  eupthsg  16440  eupth2fi  16474  nninfsellemqall  16793  qdiff  16833  gfsumcl  16870