Theorem eqtr3id 2278

Description: An equality transitivity deduction. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
eqtr3id.1	⊢ 𝐵 = 𝐴
eqtr3id.2	⊢ (𝜑 → 𝐵 = 𝐶)

Assertion

Ref	Expression
eqtr3id	⊢ (𝜑 → 𝐴 = 𝐶)

Proof of Theorem eqtr3id

Step	Hyp	Ref	Expression
1		eqtr3id.1	. . 3 ⊢ 𝐵 = 𝐴
2	1	eqcomi 2235	. 2 ⊢ 𝐴 = 𝐵
3		eqtr3id.2	. 2 ⊢ (𝜑 → 𝐵 = 𝐶)
4	2, 3	eqtrid 2276	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 2213

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

This theorem is referenced by:  3eqtr3g  2287  csbeq1a  3137  ssdifeq0  3579  pofun  4415  opabbi2dv  4885  funimaexg  5421  fresin  5523  f1imacnv  5609  foimacnv  5610  fsn2  5829  fmptpr  5854  funiunfvdm  5914  funiunfvdmf  5915  fcof1o  5940  f1opw2  6239  fnexALT  6282  eqerlem  6776  pmresg  6888  mapsn  6902  en2  7041  fopwdom  7065  mapen  7075  fiintim  7166  xpfi  7167  sbthlemi8  7206  sbthlemi9  7207  ctssdccl  7353  exmidfodomrlemim  7455  mul02  8608  recdivap  8940  fzpreddisj  10351  fzshftral  10388  suprzubdc  10542  qbtwnrelemcalc  10561  frec2uzrdg  10717  frecuzrdgrcl  10718  frecuzrdgsuc  10722  frecuzrdgrclt  10723  frecuzrdgg  10724  seqf1oglem2  10828  binom3  10965  bcn2  11072  hashfz1  11091  hashunlem  11113  hashfacen  11146  hashtpg  11157  cnrecnv  11533  resqrexlemnm  11641  amgm2  11741  2zsupmax  11849  xrmaxltsup  11881  xrmaxadd  11884  xrbdtri  11899  fisumss  12016  fsumcnv  12061  telfsumo  12090  fsumiun  12101  arisum2  12123  fprodssdc  12214  fprodsplitdc  12220  fprodsplit  12221  fprodcnv  12249  ege2le3  12295  efgt1p  12320  cos01bnd  12382  dfgcd3  12644  eucalgval  12689  sqrt2irrlem  12796  pcid  12960  4sqlem15  13041  4sqlem16  13042  setsslid  13196  ressinbasd  13220  xpsff1o  13495  grpressid  13707  crng2idl  14610  znleval  14732  baspartn  14844  txdis1cn  15072  cnmpt21  15085  cnmpt22  15088  hmeores  15109  metreslem  15174  remetdval  15341  dvfvalap  15475  binom4  15773  mpodvdsmulf1o  15787  perfectlem2  15797  1lgs  15845  lgs1  15846  lgseisenlem1  15872  lgseisenlem2  15873  lgseisenlem3  15874  lgsquadlem2  15880  lgsquad2lem2  15884  vtxdfifiun  16221  vtxdumgrfival  16222  nninfsellemqall  16724  nninfnfiinf  16732  repiecege0  16742