Theorem eqtr3id 2276

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

Syntax hints:   → wi 4   = wceq 1395

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 1493  ax-gen 1495  ax-4 1556  ax-17 1572  ax-ext 2211

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

This theorem is referenced by:  3eqtr3g  2285  csbeq1a  3133  ssdifeq0  3574  pofun  4403  opabbi2dv  4871  funimaexg  5405  fresin  5506  f1imacnv  5591  foimacnv  5592  fsn2  5811  fmptpr  5835  funiunfvdm  5893  funiunfvdmf  5894  fcof1o  5919  f1opw2  6218  fnexALT  6262  eqerlem  6719  pmresg  6831  mapsn  6845  en2  6981  fopwdom  7005  mapen  7015  fiintim  7104  xpfi  7105  sbthlemi8  7142  sbthlemi9  7143  ctssdccl  7289  exmidfodomrlemim  7390  mul02  8544  recdivap  8876  fzpreddisj  10279  fzshftral  10316  suprzubdc  10468  qbtwnrelemcalc  10487  frec2uzrdg  10643  frecuzrdgrcl  10644  frecuzrdgsuc  10648  frecuzrdgrclt  10649  frecuzrdgg  10650  seqf1oglem2  10754  binom3  10891  bcn2  10998  hashfz1  11017  hashunlem  11038  hashfacen  11071  cnrecnv  11436  resqrexlemnm  11544  amgm2  11644  2zsupmax  11752  xrmaxltsup  11784  xrmaxadd  11787  xrbdtri  11802  fisumss  11918  fsumcnv  11963  telfsumo  11992  fsumiun  12003  arisum2  12025  fprodssdc  12116  fprodsplitdc  12122  fprodsplit  12123  fprodcnv  12151  ege2le3  12197  efgt1p  12222  cos01bnd  12284  dfgcd3  12546  eucalgval  12591  sqrt2irrlem  12698  pcid  12862  4sqlem15  12943  4sqlem16  12944  setsslid  13098  ressinbasd  13122  xpsff1o  13397  grpressid  13609  crng2idl  14510  znleval  14632  baspartn  14739  txdis1cn  14967  cnmpt21  14980  cnmpt22  14983  hmeores  15004  metreslem  15069  remetdval  15236  dvfvalap  15370  binom4  15668  mpodvdsmulf1o  15679  perfectlem2  15689  1lgs  15737  lgs1  15738  lgseisenlem1  15764  lgseisenlem2  15765  lgseisenlem3  15766  lgsquadlem2  15772  lgsquad2lem2  15776  vtxdfifiun  16056  vtxdumgrfival  16057  nninfsellemqall  16441  nninfnfiinf  16449