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  4827  csbcnvg  4861  dfiun3g  4934  dfiin3g  4935  resima2  4992  relcnvfld  5215  uniabio  5241  fntpg  5329  dffn5im  5623  dfimafn2  5627  fncnvima2  5700  fmptcof  5746  fcoconst  5750  fnasrng  5759  funopsn  5761  ffnov  6048  fnovim  6053  fnrnov  6091  foov  6092  funimassov  6095  ovelimab  6096  ofc12  6181  caofinvl  6183  dftpos3  6347  tfr0dm  6407  rdgisucinc  6470  oasuc  6549  ecinxp  6696  phplem1  6948  exmidpw  7004  exmidpweq  7005  unfiin  7022  fidcenumlemr  7056  0ct  7208  ctmlemr  7209  exmidaclem  7319  indpi  7454  nqnq0pi  7550  nq0m0r  7568  addnqpr1  7674  recexgt0sr  7885  suplocsrlempr  7919  recidpipr  7968  recidpirq  7970  axrnegex  7991  nntopi  8006  cnref1o  9771  fztp  10199  fseq1m1p1  10216  fz0to4untppr  10245  frecuzrdgrrn  10551  frecuzrdgsuc  10557  frecuzrdgsuctlem  10566  seq3val  10603  seqvalcd  10604  fser0const  10678  mulexpzap  10722  expaddzap  10726  bcp1m1  10908  hash2en  10986  iswrdiz  10999  cjexp  11146  rexuz3  11243  bdtri  11493  climconst  11543  sumfct  11627  zsumdc  11637  fsum3  11640  sum0  11641  fsumcnv  11690  mertenslem2  11789  zproddc  11832  fprodseq  11836  prod0  11838  prod1dc  11839  prodfct  11840  fprodcnv  11878  ef0lem  11913  efzval  11936  efival  11985  sinbnd  12005  cosbnd  12006  eucalgval  12318  eucalginv  12320  eucalglt  12321  eucalgcvga  12322  eucalg  12323  sqpweven  12439  2sqpwodd  12440  dfphi2  12484  phimullem  12489  prmdiv  12499  odzval  12506  pcval  12561  pczpre  12562  pcrec  12573  4sqlem17  12672  ennnfonelemhdmp1  12722  ennnfonelemkh  12725  ressinbasd  12848  restid2  13022  topnvalg  13025  prdsval  13047  prdsbas3  13061  pwsval  13065  pwsbas  13066  pwselbasb  13067  pwsplusgval  13069  pwsmulrval  13070  imasival  13080  imasplusg  13082  qusval  13097  xpsval  13126  ismgm  13131  plusffvalg  13136  grpidvalg  13147  igsumvalx  13163  issgrp  13177  ismnddef  13192  pws0g  13225  ismhm  13235  isgrp  13280  grpn0  13309  grpinvfvalg  13316  grpsubfvalg  13319  pwsinvg  13386  mulgfvalg  13399  mulgval  13400  mulgnn0p1  13411  issubg  13451  isnsg  13480  eqgfval  13500  quseccl0g  13509  isghm  13521  conjsubg  13555  conjsubgen  13556  iscmn  13571  mgpvalg  13627  isrng  13638  issrg  13669  isring  13704  iscrng  13707  opprvalg  13773  dfrhm2  13858  isnzr  13885  islring  13896  issubrg  13925  rrgval  13966  isdomn  13973  islmod  13995  scaffvalg  14010  lsssetm  14060  lspfval  14092  2idlval  14206  2idlvalg  14207  mulgrhm2  14314  zlmval  14331  znval  14340  znzrhfo  14352  znle2  14356  psrval  14370  mplvalcoe  14394  istps  14446  cldval  14513  ntrfval  14514  clsfval  14515  neifval  14554  restbasg  14582  tgrest  14583  txval  14669  upxp  14686  uptx  14688  txrest  14690  lmcn2  14694  cnmpt2t  14707  cnmpt2res  14711  imasnopn  14713  psmetxrge0  14746  xmetge0  14779  isxms  14865  isms  14867  bdxmet  14915  qtopbasss  14935  cnblcld  14949  mpomulcn  14980  negfcncf  15020  dvfvalap  15095  eldvap  15096  dvidlemap  15105  dvidrelem  15106  dvidsslem  15107  dvexp2  15126  dvrecap  15127  dveflem  15140  plyconst  15159  plycolemc  15172  sin0pilem1  15195  ptolemy  15238  coskpi  15262  logbrec  15374  mpodvdsmulf1o  15404  fsumdvdsmul  15405  lgslem1  15419  lgsval  15423  lgsval4  15439  lgsfcl3  15440  lgsdilem  15446  lgsdir2lem4  15450  lgsdir2lem5  15451  gausslemma2dlem5  15485  lgsquadlem2  15497  nninfsellemqall  15885