Theorem eqtr3id 2251

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

Syntax hints:   → wi 4   = wceq 1372

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 1469  ax-gen 1471  ax-4 1532  ax-17 1548  ax-ext 2186

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

This theorem is referenced by:  3eqtr3g  2260  csbeq1a  3101  ssdifeq0  3542  pofun  4357  opabbi2dv  4825  funimaexg  5352  fresin  5448  f1imacnv  5533  foimacnv  5534  fsn2  5748  fmptpr  5766  funiunfvdm  5822  funiunfvdmf  5823  fcof1o  5848  f1opw2  6142  fnexALT  6186  eqerlem  6641  pmresg  6753  mapsn  6767  fopwdom  6915  mapen  6925  fiintim  7010  xpfi  7011  sbthlemi8  7048  sbthlemi9  7049  ctssdccl  7195  exmidfodomrlemim  7291  mul02  8441  recdivap  8773  fzpreddisj  10175  fzshftral  10212  suprzubdc  10360  qbtwnrelemcalc  10379  frec2uzrdg  10535  frecuzrdgrcl  10536  frecuzrdgsuc  10540  frecuzrdgrclt  10541  frecuzrdgg  10542  seqf1oglem2  10646  binom3  10783  bcn2  10890  hashfz1  10909  hashunlem  10930  hashfacen  10962  cnrecnv  11140  resqrexlemnm  11248  amgm2  11348  2zsupmax  11456  xrmaxltsup  11488  xrmaxadd  11491  xrbdtri  11506  fisumss  11622  fsumcnv  11667  telfsumo  11696  fsumiun  11707  arisum2  11729  fprodssdc  11820  fprodsplitdc  11826  fprodsplit  11827  fprodcnv  11855  ege2le3  11901  efgt1p  11926  cos01bnd  11988  dfgcd3  12250  eucalgval  12295  sqrt2irrlem  12402  pcid  12566  4sqlem15  12647  4sqlem16  12648  setsslid  12802  ressinbasd  12825  xpsff1o  13099  grpressid  13311  crng2idl  14211  znleval  14333  baspartn  14440  txdis1cn  14668  cnmpt21  14681  cnmpt22  14684  hmeores  14705  metreslem  14770  remetdval  14937  dvfvalap  15071  binom4  15369  mpodvdsmulf1o  15380  perfectlem2  15390  1lgs  15438  lgs1  15439  lgseisenlem1  15465  lgseisenlem2  15466  lgseisenlem3  15467  lgsquadlem2  15473  lgsquad2lem2  15477  nninfsellemqall  15816  nninfnfiinf  15824