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 1397

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 1495  ax-gen 1497  ax-4 1558  ax-17 1574  ax-ext 2213

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

This theorem is referenced by:  3eqtr3g  2287  csbeq1a  3136  ssdifeq0  3577  pofun  4409  opabbi2dv  4879  funimaexg  5414  fresin  5515  f1imacnv  5600  foimacnv  5601  fsn2  5821  fmptpr  5845  funiunfvdm  5903  funiunfvdmf  5904  fcof1o  5929  f1opw2  6228  fnexALT  6272  eqerlem  6732  pmresg  6844  mapsn  6858  en2  6997  fopwdom  7021  mapen  7031  fiintim  7122  xpfi  7123  sbthlemi8  7162  sbthlemi9  7163  ctssdccl  7309  exmidfodomrlemim  7411  mul02  8565  recdivap  8897  fzpreddisj  10305  fzshftral  10342  suprzubdc  10495  qbtwnrelemcalc  10514  frec2uzrdg  10670  frecuzrdgrcl  10671  frecuzrdgsuc  10675  frecuzrdgrclt  10676  frecuzrdgg  10677  seqf1oglem2  10781  binom3  10918  bcn2  11025  hashfz1  11044  hashunlem  11066  hashfacen  11099  cnrecnv  11470  resqrexlemnm  11578  amgm2  11678  2zsupmax  11786  xrmaxltsup  11818  xrmaxadd  11821  xrbdtri  11836  fisumss  11952  fsumcnv  11997  telfsumo  12026  fsumiun  12037  arisum2  12059  fprodssdc  12150  fprodsplitdc  12156  fprodsplit  12157  fprodcnv  12185  ege2le3  12231  efgt1p  12256  cos01bnd  12318  dfgcd3  12580  eucalgval  12625  sqrt2irrlem  12732  pcid  12896  4sqlem15  12977  4sqlem16  12978  setsslid  13132  ressinbasd  13156  xpsff1o  13431  grpressid  13643  crng2idl  14544  znleval  14666  baspartn  14773  txdis1cn  15001  cnmpt21  15014  cnmpt22  15017  hmeores  15038  metreslem  15103  remetdval  15270  dvfvalap  15404  binom4  15702  mpodvdsmulf1o  15713  perfectlem2  15723  1lgs  15771  lgs1  15772  lgseisenlem1  15798  lgseisenlem2  15799  lgseisenlem3  15800  lgsquadlem2  15806  lgsquad2lem2  15810  vtxdfifiun  16147  vtxdumgrfival  16148  nninfsellemqall  16617  nninfnfiinf  16625