Theorem eqtr3id 2240

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

Syntax hints:   → wi 4   = wceq 1364

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 1458  ax-gen 1460  ax-4 1521  ax-17 1537  ax-ext 2175

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

This theorem is referenced by:  3eqtr3g  2249  csbeq1a  3090  ssdifeq0  3530  pofun  4344  opabbi2dv  4812  funimaexg  5339  fresin  5433  f1imacnv  5518  foimacnv  5519  fsn2  5733  fmptpr  5751  funiunfvdm  5807  funiunfvdmf  5808  fcof1o  5833  f1opw2  6126  fnexALT  6165  eqerlem  6620  pmresg  6732  mapsn  6746  fopwdom  6894  mapen  6904  fiintim  6987  xpfi  6988  sbthlemi8  7025  sbthlemi9  7026  ctssdccl  7172  exmidfodomrlemim  7263  mul02  8408  recdivap  8739  fzpreddisj  10140  fzshftral  10177  qbtwnrelemcalc  10327  frec2uzrdg  10483  frecuzrdgrcl  10484  frecuzrdgsuc  10488  frecuzrdgrclt  10489  frecuzrdgg  10490  seqf1oglem2  10594  binom3  10731  bcn2  10838  hashfz1  10857  hashunlem  10878  hashfacen  10910  cnrecnv  11057  resqrexlemnm  11165  amgm2  11265  2zsupmax  11372  xrmaxltsup  11404  xrmaxadd  11407  xrbdtri  11422  fisumss  11538  fsumcnv  11583  telfsumo  11612  fsumiun  11623  arisum2  11645  fprodssdc  11736  fprodsplitdc  11742  fprodsplit  11743  fprodcnv  11771  ege2le3  11817  efgt1p  11842  cos01bnd  11904  suprzubdc  12092  dfgcd3  12150  eucalgval  12195  sqrt2irrlem  12302  pcid  12465  4sqlem15  12546  4sqlem16  12547  setsslid  12672  ressinbasd  12695  xpsff1o  12935  grpressid  13136  crng2idl  14030  znleval  14152  baspartn  14229  txdis1cn  14457  cnmpt21  14470  cnmpt22  14473  hmeores  14494  metreslem  14559  remetdval  14726  dvfvalap  14860  binom4  15152  1lgs  15200  lgs1  15201  lgseisenlem1  15227  lgseisenlem2  15228  lgseisenlem3  15229  lgsquadlem2  15235  lgsquad2lem2  15239  nninfsellemqall  15575