Theorem eqtr3id 2281

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 2238	. 2 ⊢ 𝐴 = 𝐵
3		eqtr3id.2	. 2 ⊢ (𝜑 → 𝐵 = 𝐶)
4	2, 3	eqtrid 2279	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 2216

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

This theorem is referenced by:  3eqtr3g  2290  csbeq1a  3150  ssdifeq0  3596  pofun  4438  opabbi2dv  4909  funimaexg  5445  fresin  5548  f1imacnv  5636  foimacnv  5637  fsn2  5856  fmptpr  5881  funiunfvdm  5942  funiunfvdmf  5943  fcof1o  5968  f1opw2  6269  fnexALT  6313  eqerlem  6811  pmresg  6923  mapsn  6938  en2  7078  fopwdom  7102  mapen  7112  fiintim  7204  xpfi  7205  sbthlemi8  7247  sbthlemi9  7248  ctssdccl  7415  exmidfodomrlemim  7517  mul02  8677  recdivap  9009  fzpreddisj  10427  fzshftral  10464  suprzubdc  10620  qbtwnrelemcalc  10639  frec2uzrdg  10795  frecuzrdgrcl  10796  frecuzrdgsuc  10800  frecuzrdgrclt  10801  frecuzrdgg  10802  seqf1oglem2  10906  binom3  11043  bcn2  11151  hashfz1  11171  hashunlem  11193  hashfacen  11233  hashtpg  11244  cnrecnv  11620  resqrexlemnm  11728  amgm2  11828  2zsupmax  11936  xrmaxltsup  11968  xrmaxadd  11971  xrbdtri  11986  fisumss  12103  fsumcnv  12148  telfsumo  12177  fsumiun  12188  arisum2  12210  fprodssdc  12301  fprodsplitdc  12307  fprodsplit  12308  fprodcnv  12336  ege2le3  12382  efgt1p  12407  cos01bnd  12469  dfgcd3  12731  eucalgval  12776  sqrt2irrlem  12883  pcid  13047  4sqlem15  13128  4sqlem16  13129  ballotfilemic  13194  setsslid  13347  ressinbasd  13371  xpsff1o  13613  grpressid  13816  crng2idl  14805  znleval  14927  baspartn  15041  txdis1cn  15269  cnmpt21  15282  cnmpt22  15285  hmeores  15306  metreslem  15371  remetdval  15538  dvfvalap  15672  binom4  15970  mpodvdsmulf1o  15984  perfectlem2  15994  1lgs  16042  lgs1  16043  lgseisenlem1  16069  lgseisenlem2  16070  lgseisenlem3  16071  lgsquadlem2  16077  lgsquad2lem2  16081  vtxdfifiun  16418  vtxdumgrfival  16419  nninfsellemqall  16919  nninfnfiinf  16927  repiecege0  16937